diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 6 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 8 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 6 | ||||
| -rw-r--r-- | vernac/obligations.ml | 4 |
4 files changed, 18 insertions, 6 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 7dd5471f3f..cf69a84b8b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -60,10 +60,10 @@ let make_bullet s = | _ -> assert false let parse_compat_version = let open Flags in function - | "8.8" -> Current + | "8.9" -> Current + | "8.8" -> V8_8 | "8.7" -> V8_7 - | "8.6" -> V8_6 - | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + | ("8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> CErrors.user_err ~hdr:"get_compat_version" Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") | s -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 880a11becd..aa9bd20bf3 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -344,6 +344,14 @@ let universe_proof_terminator compute_guard hook = let standard_proof_terminator compute_guard hook = universe_proof_terminator compute_guard (fun _ -> hook) +let initialize_named_context_for_proof () = + let sign = Global.named_context () in + List.fold_right + (fun d signv -> + let id = NamedDecl.get_id d in + let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in + Environ.push_named_context_val d signv) sign Environ.empty_named_context_val + let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = let terminator = match terminator with | None -> standard_proof_terminator compute_guard hook diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index c9e4876ee3..38683ed6b2 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -56,6 +56,11 @@ val standard_proof_terminator : val fresh_name_for_anonymous_theorem : unit -> Id.t +(* Prepare global named context for proof session: remove proofs of + opaque section definitions and remove vm-compiled code *) + +val initialize_named_context_for_proof : unit -> Environ.named_context_val + (** {6 ... } *) (** A hook the next three functions pass to cook_proof *) @@ -63,7 +68,6 @@ val set_save_hook : (Proof.t -> unit) -> unit val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit - (** [get_current_context ()] returns the evar context and env of the current open proof if any, otherwise returns the empty evar context and the current global env *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 3987e53bc7..c4a10b4be6 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1102,7 +1102,7 @@ let show_term n = let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = - let sign = Decls.initialize_named_context_for_proof () in + let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in @@ -1122,7 +1122,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = - let sign = Decls.initialize_named_context_for_proof () in + let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> |