From: Claudio Sacerdoti Coen Date: Sat, 7 Feb 2004 17:52:01 +0000 (+0000) Subject: sort_of_prod: the second term, when it is a meta, was unified with a fresh X-Git-Tag: V_0_2_3~8 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88600f044c826df73c805e10fc9f8e6d4a3921bf;p=helm.git sort_of_prod: the second term, when it is a meta, was unified with a fresh meta in a wrong context. Fixed. --- diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 43ecd8929..42d792d98 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -466,8 +466,9 @@ and type_of_aux' metasenv context t = and sort_of_prod subst metasenv context (name,s) (t1, t2) = let module C = Cic in + let context_for_t2 = (Some (name,C.Decl s))::context in let t1'' = CicMetaSubst.whd subst context t1 in - let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in + let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in match (t1'', t2'') with (C.Sort s1, C.Sort s2) when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *) @@ -485,7 +486,7 @@ and type_of_aux' metasenv context t = let (metasenv,idx) = CicMkImplicit.mk_implicit metasenv [] in let (subst, metasenv) = - CicUnification.fo_unif_subst subst context metasenv + CicUnification.fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' in t2'',subst,metasenv