diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-14 14:11:12 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-14 14:11:12 +0000 |
| commit | ba5a8de5013093f00c13fcabea9ba79781a496b4 (patch) | |
| tree | 659ac30acf00465b873ce9ee3d23e1a0284e1918 /interp | |
| parent | fb3359d1fdd572066f17c70c33b22e88e71a0a3f (diff) | |
correction bug de choix de noms courts avec Suresnes/BDD
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5476 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e0b39d799..b0dd97fa4 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1620,8 +1620,8 @@ let rec extern inctx scopes vars r = let (ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in - (fi,nv.(i), bl, extern_type scopes vars1 ty, - extern false scopes vars0 def)) idv + (fi,nv.(i), bl, extern_type scopes vars0 ty, + extern false scopes vars1 def)) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) | RCoFix n -> @@ -1630,8 +1630,8 @@ let rec extern inctx scopes vars r = let (ids,bl) = extern_local_binder scopes vars blv.(i) in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in - (fi,bl,extern_type scopes vars1 tyv.(i), - sub_extern false scopes vars0 bv.(i))) idv + (fi,bl,extern_type scopes vars0 tyv.(i), + sub_extern false scopes vars1 bv.(i))) idv in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) |