diff options
| author | Gaëtan Gilbert | 2018-09-03 14:37:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-03 14:37:12 +0200 |
| commit | c880e9e01d57eb4beca561e209839caa66d38742 (patch) | |
| tree | 87752aad1c8aab7afece5d83f4d38175d0f2768c /vernac | |
| parent | bb5c4eee0807cd988d236d4538a2fa2f05ef0daf (diff) | |
| parent | 6d998b5a0e6090b5c7d87d575016adc127b666d9 (diff) | |
Merge PR #891: Check universes are declared
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 b9c47ff475..a4650cfd92 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -679,6 +679,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 @@ -716,6 +721,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 @@ -1299,6 +1306,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)) -> |