In Univ, unify order_request and constraint_type

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

2 files changed, 11 insertions, 13 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index da6f2e1791..4b865fab9a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -381,9 +381,9 @@ let merge_disc g u v =
 (* Universe inconsistency: error raised when trying to enforce a relation
    that would create a cycle in the graph of universes. *)
 
-type order_request = Lt | Le | Eq
+type constraint_type = Lt | Le | Eq
 
-exception UniverseInconsistency of order_request * universe * universe
+exception UniverseInconsistency of constraint_type * universe * universe
 
 let error_inconsistency o u v = raise (UniverseInconsistency (o,Atom u,Atom v))
 
@@ -447,14 +447,12 @@ let merge_universes sp u1 u2 =
 
 (* Constraints and sets of consrtaints. *)
 
-type constraint_type = Lt | Leq | Eq
-
 type univ_constraint = universe_level * constraint_type * universe_level
 
 let enforce_constraint cst g =
   match cst with
     | (u,Lt,v) -> enforce_univ_lt u v g
-    | (u,Leq,v) -> enforce_univ_leq u v g
+    | (u,Le,v) -> enforce_univ_leq u v g
     | (u,Eq,v) -> enforce_univ_eq u v g
 
 
@@ -470,7 +468,7 @@ type constraint_function =
     universe -> universe -> constraints -> constraints
 
 let constraint_add_leq v u c =
-  if v = Set then c else Constraint.add (v,Leq,u) c
+  if v = Set then c else Constraint.add (v,Le,u) c
 
 let enforce_geq u v c =
   match u, v with
@@ -589,7 +587,7 @@ let pr_constraints c =
   Constraint.fold (fun (u1,op,u2) pp_std ->
 		     let op_str = match op with
 		       | Lt -> " < "
-		       | Leq -> " <= "
+		       | Le -> " <= "
 		       | Eq -> " = "
 		     in pp_std ++  pr_uni_level u1 ++ str op_str ++
 			  pr_uni_level u2 ++ fnl () )  c (str "")
@@ -600,10 +598,10 @@ let dump_universes output g =
   let dump_arc _ = function
     | Canonical {univ=u; lt=lt; le=le} ->
 	let u_str = string_of_univ_level u in
-	List.iter (fun v -> output `Lt u_str (string_of_univ_level v)) lt;
-	List.iter (fun v -> output `Le u_str (string_of_univ_level v)) le
+	List.iter (fun v -> output Lt u_str (string_of_univ_level v)) lt;
+	List.iter (fun v -> output Le u_str (string_of_univ_level v)) le
     | Equiv (u,v) ->
-      output `Eq (string_of_univ_level u) (string_of_univ_level v)
+      output Eq (string_of_univ_level u) (string_of_univ_level v)
   in
     UniverseLMap.iter dump_arc g
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 85e2278911..e9f25fe851 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -57,9 +57,9 @@ val enforce_eq : constraint_function
   universes graph. It raises the exception [UniverseInconsistency] if the
   constraints are not satisfiable. *)
 
-type order_request = Lt | Le | Eq
+type constraint_type = Lt | Le | Eq
 
-exception UniverseInconsistency of order_request * universe * universe
+exception UniverseInconsistency of constraint_type * universe * universe
 
 val merge_constraints : constraints -> universes -> universes
 
@@ -86,7 +86,7 @@ val pr_constraints : constraints -> Pp.std_ppcmds
 (** {6 Dumping to a file } *)
 
 val dump_universes :
-  ([> `Lt | `Le | `Eq ] -> string -> string -> unit) ->
+  (constraint_type -> string -> string -> unit) ->
   universes -> unit
 
 val hcons1_univ : universe -> universe