From 75a7e852a03cdaa788e7005dfce222c5d6359915 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 15 Jun 2005 14:41:07 +0000 Subject: [PATCH] Bug fixed (that used to throw away a metasenv :-( --- helm/ocaml/cic_unification/cicRefine.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 47d186dcb..f30e3c53c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -1045,7 +1045,7 @@ let typecheck metasenv uri obj = let t = CicSubstitution.subst t' t in i - 1,t ) tys (typesno - 1,t)) in - let ty' = undebrujin ty in + let ty' = undebrujin ty' in metasenv,ugraph,(name,ty')::res ) cl (metasenv,ugraph,[]) in -- 2.39.2