diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
| commit | cdcb658c29409c8aef94ca3e22c14a90b396aea0 (patch) | |
| tree | 8981d0a2312604c6b8ab8a8acb108f39f1cd1377 /backend/RTLtypingaux.ml | |
| parent | f535ac931c2b7dc65fefa83e47bb8c79ca90e92d (diff) | |
| download | compcert-cdcb658c29409c8aef94ca3e22c14a90b396aea0.tar.gz compcert-cdcb658c29409c8aef94ca3e22c14a90b396aea0.zip | |
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
Diffstat (limited to 'backend/RTLtypingaux.ml')
| -rw-r--r-- | backend/RTLtypingaux.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |