From: Andrea Asperti Date: Tue, 16 Mar 2004 17:50:08 +0000 (+0000) Subject: Sorts are no longer all convertible. To be completed once that universes are X-Git-Tag: v0_0_4~13 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9a56298c7e6cfd34830ab40393b880f5a678e98d;p=helm.git Sorts are no longer all convertible. To be completed once that universes are implemented. --- diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 36a25a6c2..14c69a457 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -308,6 +308,7 @@ and type_of_aux' metasenv context t = The easy case is when the outype is specified, that amount to a trivial check. Otherwise, we should guess a type from its instances *) + (* easy case *) let _, subst, metasenv = type_of_aux subst metasenv context @@ -548,7 +549,7 @@ and type_of_aux' metasenv context t = (match hetype with Cic.Prod (n,s,t) -> let subst,metasenv = - fo_unif_subst subst context metasenv s hety + fo_unif_subst subst context metasenv hety s in eat_prods metasenv subst context (CicMetaSubst.subst subst hete t) tl @@ -559,7 +560,6 @@ and type_of_aux' metasenv context t = eat_prods metasenv subst context hetype' tlbody_and_type in t,subst,metasenv - (* let rec aux context' args (resty,subst,metasenv) = function @@ -608,7 +608,6 @@ and type_of_aux' metasenv context t = in aux [] [] (hetype,subst,metasenv) tlbody_and_type *) - in let ty,subst',metasenv' = type_of_aux [] metasenv context t