diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-26 13:35:24 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-26 13:35:24 +0000 |
| commit | 67fe536720c5ef5bb509249b9a30cbc6f2cebd92 (patch) | |
| tree | 54964d8e58b41b401d097f044d50b03ee68da118 /interp/constrextern.ml | |
| parent | e6370d38bd56ccd070cb33d257147ace238efc8b (diff) | |
Keep structure information for Fixpoint declaration and Fix terms
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e28065afd..fa1faf9cf 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1009,7 +1009,7 @@ let rec check_same_type ty1 ty2 = match ty1, ty2 with | CRef r1, CRef r2 -> check_same_ref r1 r2 | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 -> - List.iter2 (fun (id1,i1,a1,b1) (id2,i2,a2,b2) -> + List.iter2 (fun (id1,i1,_,a1,b1) (id2,i2,_,a2,b2) -> if id1<>id2 || i1<>i2 then failwith "not same fix"; check_same_type a1 a2; check_same_type b1 b2) @@ -1508,7 +1508,7 @@ let rec extern inctx scopes vars r = | RFix (nv,n) -> let listdecl = Array.mapi (fun i fi -> - (fi,nv.(i),extern_type scopes vars tyv.(i), + (fi,nv.(i), None, extern_type scopes vars tyv.(i), extern false scopes vars' bv.(i))) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) |