From c02c3be6892f0f4bfdad52e9d5431ee0a5a69216 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 12 Apr 2007 12:11:11 +0000 Subject: [PATCH] HACK for indtype checking --- helm/software/components/cic_unification/cicRefine.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2