diff options
| author | Matthieu Sozeau | 2017-07-20 15:45:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-07-25 17:56:21 +0200 |
| commit | cba9f3fe48817e8e524483fd984ea4938b3dc14f (patch) | |
| tree | 5ccc7b8297975c777e48d69c9918b0cb91fb9d19 /vernac | |
| parent | 9b6ce4f1848c546d0d361aa1089fa2907ca4c9ad (diff) | |
kernel: missing check that all universes are declared.
Keep the universe_levels_of_constr function inside typeops, not
exported.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c49ffe2679..d2dff06ca3 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -685,6 +685,11 @@ let explain_unsatisfied_constraints env sigma cst = Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++ spc () ++ str "(maybe a bugged tactic)." +let explain_undeclared_universe env sigma l = + strbrk "Undeclared universe: " ++ + Termops.pr_evd_level sigma l ++ + spc () ++ str "(maybe a bugged tactic)." + let explain_type_error env sigma err = let env = make_all_name_different env sigma in match err with @@ -722,6 +727,8 @@ let explain_type_error env sigma err = explain_wrong_case_info env ind ci | UnsatisfiedConstraints cst -> explain_unsatisfied_constraints env sigma cst + | UndeclaredUniverse l -> + explain_undeclared_universe env sigma l let pr_position (cl,pos) = let clpos = match cl with @@ -1310,6 +1317,7 @@ let map_ptype_error f = function | IllTypedRecBody (n, na, jv, t) -> IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t) | UnsatisfiedConstraints g -> UnsatisfiedConstraints g +| UndeclaredUniverse l -> UndeclaredUniverse l let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) -> |