X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=d6504eb1584c28c5ec7abd5ff4d190e1daa7135b;hb=99ca90bf28a25fcd1cd84596c37be43c97f74e6e;hp=1490417f1f30306daf85f33c55136371b1e773e9;hpb=91793e01113bc28fbd71fd8cd7cb664341432723;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 1490417f1..d6504eb15 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/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