From e70d9b498615e473258fb1010cc65d39e27a5830 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 --- components/cic_unification/cicRefine.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2