HACK for indtype checking

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 1490417f1f30306daf85f33c55136371b1e773e9..d6504eb1584c28c5ec7abd5ff4d190e1daa7135b 100644 (file)
--- 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