From cdcb658c29409c8aef94ca3e22c14a90b396aea0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 18 Oct 2011 09:40:59 +0000 Subject: Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLtypingaux.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/RTLtypingaux.ml') diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index 17acbc6e..59356056 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -39,7 +39,7 @@ let rec set_types rl tyl = (* First pass: process constraints of the form typeof(r) = ty *) -let type_instr retty (Coq_pair(pc, i)) = +let type_instr retty (pc, i) = match i with | Inop(_) -> () @@ -48,7 +48,7 @@ let type_instr retty (Coq_pair(pc, i)) = | Iop(op, args, res, _) -> if two_address_op op && List.length args >= 1 && List.hd args <> res then raise (Type_error "two-address constraint violation"); - let (Coq_pair(targs, tres)) = type_of_operation op in + let (targs, tres) = type_of_operation op in set_types args targs; set_type res tres | Iload(chunk, addr, args, dst, _) -> set_types args (type_of_addressing addr); @@ -119,7 +119,7 @@ let type_pass1 retty instrs = let rec extract_moves = function | [] -> [] - | Coq_pair(pc, i) :: rem -> + | (pc, i) :: rem -> match i with | Iop(Omove, [r1], r2, _) -> (r1, r2) :: extract_moves rem -- cgit