diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 17b411f9f7..87d9e306fe 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -368,7 +368,7 @@ let import_constraints g sp cst = merge_constraints cst g with UniverseInconsistency -> errorlabstrm "import_constraints" - [< 'sTR "Universe Inconsistency during import of"; 'sPC; print_sp sp >] + [< 'sTR "Universe Inconsistency during import of"; 'sPC; pr_sp sp >] let import cenv env = check_imports env cenv.cenv_needed; |