From 8d5da894b55943f59ebdb98c22432933939568a8 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Sun, 26 Sep 1999 09:15:37 +0000
Subject: message erreur UI pendant import

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@79 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index a97c92a5d9..e54de389c7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Pp
 open System
 open Util
 open Names
@@ -292,6 +293,13 @@ let check_imports env needed =
   in
   List.iter check needed
 
+let import_constraints g sp cst =
+  try
+    merge_constraints cst g
+  with UniverseInconsistency ->
+    errorlabstrm "import_constraints"
+      [< 'sTR "Universe Inconsistency during import of"; 'sPC; print_sp sp >]
+
 let import cenv env =
   check_imports env cenv.cenv_needed;
   let add_list t = List.fold_left (fun t (sp,x) -> Spmap.add sp x t) t in
@@ -305,10 +313,10 @@ let import cenv env =
   in
   let g = universes env in
   let g = List.fold_left 
-	    (fun g (_,cb) -> merge_constraints cb.const_constraints g) 
+	    (fun g (sp,cb) -> import_constraints g sp cb.const_constraints) 
 	    g cenv.cenv_constants in
   let g = List.fold_left 
-	    (fun g (_,mib) -> merge_constraints mib.mind_constraints g) 
+	    (fun g (sp,mib) -> import_constraints g sp mib.mind_constraints) 
 	    g cenv.cenv_inductives in
   { env with env_globals = new_globals; env_universes = g }
 
-- 
cgit v1.2.3