From ef0da718a83ebfa1d953ad8fd53506b5657c349a Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 3 Nov 2010 09:54:06 +0000
Subject: 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
---
 kernel/univ.ml            | 18 ++++++++----------
 kernel/univ.mli           |  6 +++---
 toplevel/vernacentries.ml | 12 ++++++------
 3 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/kernel/univ.ml b/kernel/univ.ml
index da6f2e179..4b865fab9 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 85e227891..e9f25fe85 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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3244f8288..ee69f5574 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -211,11 +211,11 @@ let dump_universes s =
       begin fun kind left right ->
         let () = Lazy.force init in
         match kind with
-          | `Lt ->
+          | Univ.Lt ->
             Printf.fprintf output "  \"%s\" -> \"%s\" [style=bold];\n" right left
-          | `Le ->
+          | Univ.Le ->
             Printf.fprintf output "  \"%s\" -> \"%s\" [style=solid];\n" right left
-          | `Eq ->
+          | Univ.Eq ->
             Printf.fprintf output "  \"%s\" -> \"%s\" [style=solid];\n" left right;
             Printf.fprintf output "  \"%s\" -> \"%s\" [style=solid];\n" right left
       end, begin fun () ->
@@ -225,9 +225,9 @@ let dump_universes s =
     end else begin
       begin fun kind left right ->
         let kind = match kind with
-          | `Lt -> "<"
-          | `Le -> "<="
-          | `Eq -> "="
+          | Univ.Lt -> "<"
+          | Univ.Le -> "<="
+          | Univ.Eq -> "="
         in Printf.fprintf output "%s %s %s ;\n" left kind right
       end, (fun () -> close_out output)
     end
-- 
cgit v1.2.3