From 86b28df4c6029d43a0f12ab7c2d85cc13f4f60f1 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 6 Jun 2008 16:03:45 +0000
Subject: ajout d'un printer pour les contraintes d'univers + correction d'un
 bug sur les notations dans les alias de module.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11063 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/univ.ml  | 10 +++++++++-
 kernel/univ.mli |  1 +
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 89b4a21124..001ee3ea8a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -579,7 +579,15 @@ let pr_universes g =
   let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
   prlist (function (_,a) -> pr_arc a) graph
     
-
+let pr_constraints c =
+  Constraint.fold (fun (u1,op,u2) pp_std -> 
+		     let op_str = match op with 
+		       | Lt -> " < "
+		       | Leq -> " <= "
+		       | Eq -> " = "
+		     in pp_std ++  pr_uni_level u1 ++ str op_str ++
+			  pr_uni_level u2 ++ fnl () )  c (str "")
+    
 (* Dumping constrains to a file *)
 
 let dump_universes output g = 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e2594e217a..1ce5329ab9 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -80,6 +80,7 @@ val subst_large_constraints :
 
 val pr_uni : universe -> Pp.std_ppcmds
 val pr_universes : universes -> Pp.std_ppcmds
+val pr_constraints : constraints -> Pp.std_ppcmds
 
 (*s Dumping to a file *)
 
-- 
cgit v1.2.3