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 36a25a6c227928f4fddb099195cc508a078e42d8..14c69a4571900d956f041581595c55071def654d 100644 (file)
--- 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