diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 8 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 18 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
3 files changed, 17 insertions, 13 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)) -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ce74f2344a..880a11becd 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -71,17 +71,13 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let add c cb e = - let exists c e = - try ignore(Environ.lookup_constant c e); true - with Not_found -> false in - if exists c e then e else Environ.add_constant c cb e in - let env = List.fold_left (fun env { eff } -> - match eff with - | SEsubproof (c, cb,_) -> add c cb env - | SEscheme (l,_) -> - List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Safe_typing.side_effects_of_private_constants eff) in + let fold env eff = + try + let _ = Environ.lookup_constant eff.seff_constant env in + env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env + in + let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard env possible_indexes fixdecls in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5258ab2ea4..e1c9712135 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1505,8 +1505,8 @@ let _ = { optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; - optread = (fun () -> !CClosure.share); - optwrite = (fun b -> CClosure.share := b) } + optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); + optwrite = (fun b -> Global.set_reduction_sharing b) } let _ = declare_bool_option |