A version of Univ.check_eq with no anomaly for Evd.set_eq_sort

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

3 files changed, 17 insertions, 4 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index f0501358bc..e6752bb9eb 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -425,14 +425,25 @@ let compare_list cmp l1 l2 =
   (l1 == l2)
   || (incl_list cmp l1 l2 && incl_list cmp l2 l1)
 
-let check_eq g u v =
+(** [check_eq] is also used in [Evd.set_eq_sort],
+    hence [Evarconv] and [Unification]. In this case,
+    it seems that the Atom/Max case may occur,
+    hence a relaxed version. *)
+
+let gen_check_eq strict g u v =
   match u,v with
     | Atom ul, Atom vl -> check_equal g ul vl
     | Max(ule,ult), Max(vle,vlt) ->
         (* TODO: remove elements of lt in le! *)
         compare_list (check_equal g) ule vle &&
         compare_list (check_equal g) ult vlt
-    | _ -> anomaly (str "check_eq") (* not complete! (Atom(u) = Max([u],[]) *)
+    | _ ->
+      (* not complete! (Atom(u) = Max([u],[]) *)
+      if strict then anomaly (str "check_eq")
+      else false (* in non-strict mode, under-approximation *)
+
+let check_eq = gen_check_eq true
+let lax_check_eq = gen_check_eq false
 
 let check_leq g u v =
   match u,v with
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c74797c8b0..6b64ca8e47 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -77,6 +77,7 @@ type universes
 type check_function = universes -> universe -> universe -> bool
 val check_leq : check_function
 val check_eq : check_function
+val lax_check_eq : check_function (* same, without anomaly *)
 
 (** The empty graph of universes *)
 val initial_universes : universes
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0f709e454f..6efdf04559 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -574,8 +574,9 @@ let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
       | Type u, Type v when (is_univ_level_var us u) || (is_univ_level_var us v) ->
 	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
       | Prop c, Type u when is_univ_var_or_set u &&
-	  Univ.check_eq sm u1 u2 -> d
-      | Type u, Prop c when is_univ_var_or_set u && Univ.check_eq sm u1 u2 -> d
+	  Univ.lax_check_eq sm u1 u2 -> d
+      | Type u, Prop c when is_univ_var_or_set u &&
+          Univ.lax_check_eq sm u1 u2 -> d
       | Type u, Type v when is_univ_var_or_set u && is_univ_var_or_set v ->
 	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
       | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2, []))