univ inconsistency error message gives evidence of a cycle

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

1 files changed, 16 insertions, 1 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index a1c1bb206..c53a3c54d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -71,7 +71,22 @@ val enforce_eq : constraint_function
 
 type constraint_type = Lt | Le | Eq
 
-exception UniverseInconsistency of constraint_type * universe * universe
+(** Type explanation is used to decorate error messages to provide
+  useful explanation why a given constraint is rejected. It is composed
+  of a path of universes and relation kinds [(r1,u1);..;(rn,un)] means
+   .. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol
+  denoted by ri, currently only < and <=). The lowest end of the chain
+  is supposed known (see UniverseInconsistency exn). The upper end may
+  differ from the second univ of UniverseInconsistency because all
+  universes in the path are canonical. Note that each step does not
+  necessarily correspond to an actual constraint, but reflect how the
+  system stores the graph and may result from combination of several
+  constraints...
+*)
+type explanation = (constraint_type * universe) list
+
+exception UniverseInconsistency of
+    constraint_type * universe * universe * explanation
 
 val merge_constraints : constraints -> universes -> universes
 val normalize_universes : universes -> universes