Change unification with sort constraints to not use the kernel

conversion when sort variables are involved and always call it
with an empty sort constraint set to avoid [whd_sort_variable] reducing
a universe variable to an algebraic universe.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12156 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 16 insertions, 10 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 3c87defa0c..ecad02cd40 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -190,15 +190,15 @@ let rec canonical_find u scstr =
 let find_univ u scstr =
   try canonical_find u scstr
   with Not_found -> u, DefinedSort (Type u)
-    
+
 let whd_sort_var scstr t =
   match kind_of_term t with
       Sort(Type u) ->
         (try
           match canonical_find u scstr with
-              _, DefinedSort s -> mkSort s
-            | _ -> t
-        with Not_found -> t)
+          | _, DefinedSort s -> mkSort s
+          | _ -> t
+          with Not_found -> t)
     | _ -> t
 
 let rec set_impredicative u s scstr =
@@ -533,6 +533,7 @@ let empty =  {
 
 let evars_reset_evd evd d = {d with evars = (fst evd.evars, 
 					    EvarMap.merge_constraints (snd evd.evars) (snd d.evars))}
+
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 let evar_source evk d =
   try List.assoc evk d.history
@@ -627,6 +628,8 @@ let define_sort_variable ({evars=(sigma,sm)}as d) u s =
 let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
 let solve_sort_constraints ({evars=(sigma,sm)} as d) =
   { d with evars = (sigma, solve_sort_cstrs sm) }
+let clear_sort_constraints ({evars=(sigma,sm)} as d) =
+  { d with evars = (sigma, UniverseMap.empty) }
 
 (* This refreshes universes in types introducing sort variables;
    works only for inferred types (i.e. for
@@ -639,7 +642,11 @@ let universes_to_variables_gen strict evd t =
     | Sort (Type u as us) when strict or u <> Univ.type0m_univ ->
 	if not (is_sort_variable !evdref us) then
 	  let s', evd = new_sort_variable !evdref in
-	  let evd = set_leq_sort_variable evd s' us in
+	  let evd = 
+	    if not (Univ.is_univ_variable u) then
+	      set_leq_sort_variable evd us s'
+	    else evd
+	  in
 	    evdref := evd; modified := true; mkSort s'
 	else t
     | Prod (na,u,v) -> mkProd (na,u,refresh v)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 040cbf28c9..10ea2ca4dd 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -243,6 +243,7 @@ val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val set_eq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val solve_sort_constraints : evar_defs -> evar_defs
+val clear_sort_constraints : evar_defs -> evar_defs
 
 val universes_to_variables : evar_defs -> types -> evar_defs * types
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0f8d2b860a..6c58e247a5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -176,14 +176,13 @@ let oracle_order env cf1 cf2 =
       | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
 
 let is_trans_fconv_pb pb flags env sigma m n =
-  match pb with
-  | Cumul -> is_trans_fconv CUMUL flags env sigma m n
-  | ConvUnderApp _ -> is_trans_fconv CONV flags env sigma m n
+  let sigma' = clear_sort_constraints sigma in
+    is_trans_fconv (conv_pb_of pb) flags env sigma' m n
 
 let occur_meta_or_sortvar evd c =
   let rec occrec c = match kind_of_term c with
     | Meta _ -> raise Occur
-    | Sort s -> if Evd.is_sort_variable evd s then raise Occur
+    | Sort (Type u) -> raise Occur
     | _ -> iter_constr occrec c
   in try occrec c; false with Occur -> true
 
@@ -369,7 +368,6 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
 
   in
-  let m = whd_sort_variable sigma m and n = whd_sort_variable sigma n in
     if (if occur_meta_or_sortvar sigma m || occur_meta_or_sortvar sigma n then false else
       if (match flags.modulo_conv_on_closed_terms with
       | Some flags ->