X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_unification%2FcicRefine.ml;h=d6504eb1584c28c5ec7abd5ff4d190e1daa7135b;hb=d6a96d7ae2a320e390ce60b0ee30feebf9f2ee28;hp=1490417f1f30306daf85f33c55136371b1e773e9;hpb=481340536d31492773c34d9413122abf7fef7959;p=helm.git

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 1490417f1..d6504eb15 100644
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1734,6 +1734,7 @@ let typecheck metasenv uri obj ~localization_tbl =
      let con_context =
       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
      (* second phase: we fix only the constructors *)
+     let saved_menv = metasenv in
      let metasenv,ugraph,tys =
       List.fold_right
        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
@@ -1746,7 +1747,7 @@ let typecheck metasenv uri obj ~localization_tbl =
              let ty',_,metasenv,ugraph =
               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
              let ty' = undebrujin uri typesno tys ty' in
-              metasenv,ugraph,(name,ty')::res
+              metasenv@saved_menv,ugraph,(name,ty')::res
            ) cl (metasenv,ugraph,[])
          in
           metasenv,ugraph,(name,b,ty,cl')::res