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

2 files changed, 14 insertions, 2 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