diff options
| author | filliatr | 1999-09-26 09:15:37 +0000 |
|---|---|---|
| committer | filliatr | 1999-09-26 09:15:37 +0000 |
| commit | 8d5da894b55943f59ebdb98c22432933939568a8 (patch) | |
| tree | 0325476a12e054eb9e2ed2d2f5e91c2e7399a6e7 /kernel | |
| parent | 9084393008d9cd2a1f36391e06f6a73cbc529a16 (diff) | |
message erreur UI pendant import
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@79 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 12 |
1 files changed, 10 insertions, 2 deletions
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 } |