aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml20
-rw-r--r--vernac/command.ml4
-rw-r--r--vernac/command.mli3
-rw-r--r--vernac/indschemes.ml9
-rw-r--r--vernac/lemmas.ml10
-rw-r--r--vernac/lemmas.mli17
-rw-r--r--vernac/metasyntax.ml24
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/search.ml2
-rw-r--r--vernac/vernacentries.ml109
10 files changed, 95 insertions, 105 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index dc5ce1a53..aba61146c 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
if not (Option.is_empty term) then
let init_refine =
Tacticals.New.tclTHENLIST [
- Refine.refine (fun evm -> (evm,EConstr.of_constr (Option.get term)));
+ Refine.refine ~typecheck:false (fun evm -> (evm,EConstr.of_constr (Option.get term)));
Proofview.Unsafe.tclNEWGOALS gls;
Tactics.New.reduce_after_refine;
]
@@ -386,7 +386,13 @@ let context poly l =
let ctx = Univ.ContextSet.to_context !uctx in
(* Declare the universe context once *)
let () = uctx := Univ.ContextSet.empty in
- let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
+ let decl = match b with
+ | None ->
+ (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical)
+ | Some b ->
+ let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+ (DefinitionEntry entry, IsAssumption Logical)
+ in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
match class_of_constr !evars (EConstr.of_constr t) with
| Some (rels, ((tc,_), args) as _cl) ->
@@ -402,9 +408,17 @@ let context poly l =
in
let impl = List.exists test impls in
let decl = (Discharge, poly, Definitional) in
- let nstatus =
+ let nstatus = match b with
+ | None ->
pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
Vernacexpr.NoInline (Loc.tag id))
+ | Some b ->
+ let ctx = Univ.ContextSet.to_context !uctx in
+ let decl = (Discharge, poly, Definition) in
+ let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+ let hook = Lemmas.mk_hook (fun _ gr -> gr) in
+ let _ = Command.declare_definition id decl entry [] [] hook in
+ Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
let () = uctx := Univ.ContextSet.empty in
status && nstatus
diff --git a/vernac/command.ml b/vernac/command.ml
index b1425d703..998e7803e 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -187,7 +187,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
let () = definition_message ident in
let gr = VarRef ident in
let () = maybe_declare_manual_implicits false gr imps in
- let () = if Pfedit.refining () then
+ let () = if Proof_global.there_are_pending_proofs () then
warn_definition_not_visible ident
in
gr
@@ -233,7 +233,7 @@ match local with
let _ = declare_variable ident decl in
let () = assumption_message ident in
let () =
- if not !Flags.quiet && Pfedit.refining () then
+ if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
strbrk " is not visible from current goals")
in
diff --git a/vernac/command.mli b/vernac/command.mli
index 9bbc2fdac..2a52d9bcb 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -15,7 +15,6 @@ open Vernacexpr
open Constrexpr
open Decl_kinds
open Redexpr
-open Pfedit
(** This file is about the interpretation of raw commands into typed
ones and top-level declaration of the main Gallina objects *)
@@ -151,7 +150,7 @@ val declare_fixpoint :
locality -> polymorphic ->
recursive_preentry * lident list option * Evd.evar_universe_context *
(Context.Rel.t * Impargs.manual_implicits * int option) list ->
- lemma_possible_guards -> decl_notation list -> unit
+ Proof_global.lemma_possible_guards -> decl_notation list -> unit
val declare_cofixpoint : locality -> polymorphic ->
recursive_preentry * lident list option * Evd.evar_universe_context *
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c2c27eb78..44d6f37cc 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -84,15 +84,8 @@ let _ =
optkey = ["Boolean";"Equality";"Schemes"];
optread = (fun () -> !eq_flag) ;
optwrite = (fun b -> eq_flag := b) }
-let _ = (* compatibility *)
- declare_bool_option
- { optdepr = true;
- optname = "automatic declaration of boolean equality";
- optkey = ["Equality";"Scheme"];
- optread = (fun () -> !eq_flag) ;
- optwrite = (fun b -> eq_flag := b) }
-let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
+let is_eq_flag () = !eq_flag
let eq_dec_flag = ref false
let _ =
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 77e356eb2..5bf419caf 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -209,7 +209,7 @@ let compute_proof_name locality = function
user_err ?loc (pr_id id ++ str " already exists.");
id, pl
| None ->
- next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
+ next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None
let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
let t_i = norm t_i in
@@ -487,7 +487,7 @@ let save_proof ?proof = function
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
| None ->
- let pftree = Pfedit.get_pftreestate () in
+ let pftree = Proof_global.give_me_the_proof () in
let id, k, typ = Pfedit.current_proof_statement () in
let typ = EConstr.Unsafe.to_constr typ in
let universes = Proof.initial_euctx pftree in
@@ -496,7 +496,7 @@ let save_proof ?proof = function
Proof_global.return_proof ~allow_partial:true () in
let sec_vars =
if not !keep_admitted_vars then None
- else match Pfedit.get_used_variables(), pproofs with
+ else match Proof_global.get_used_variables(), pproofs with
| Some _ as x, _ -> x
| None, (pproof, _) :: _ ->
let env = Global.env () in
@@ -504,7 +504,7 @@ let save_proof ?proof = function
let ids_def = Environ.global_vars_set env pproof in
Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
| _ -> None in
- let names = Pfedit.get_universe_binders () in
+ let names = Proof_global.get_universe_binders () in
let evd = Evd.from_ctx universes in
let binders, ctx = Evd.universe_context ?names evd in
Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
@@ -519,7 +519,7 @@ let save_proof ?proof = function
| Some proof -> proof
in
(* if the proof is given explicitly, nothing has to be deleted *)
- if Option.is_empty proof then Pfedit.delete_current_proof ();
+ if Option.is_empty proof then Proof_global.discard_current ();
Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
(* Miscellaneous *)
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index d06b8fd14..a9c0d99f3 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -9,7 +9,6 @@
open Names
open Term
open Decl_kinds
-open Pfedit
type 'a declaration_hook
val mk_hook :
@@ -21,16 +20,16 @@ val call_hook :
(** A hook start_proof calls on the type of the definition being started *)
val set_start_hook : (EConstr.types -> unit) -> unit
-val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
- ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
+val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+ ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
+ ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
unit declaration_hook -> unit
-val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
- ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+ ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
+ ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
(Evd.evar_universe_context option -> unit declaration_hook) -> unit
val start_proof_com :
@@ -40,8 +39,8 @@ val start_proof_com :
val start_proof_with_initialization :
goal_kind -> Evd.evar_map ->
- (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
- ((Id.t (* name of thm *) * universe_binders option) *
+ (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
+ ((Id.t (* name of thm *) * Proof_global.universe_binders option) *
(types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
-> int list option -> unit declaration_hook -> unit
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 34b9b97d8..a114553cd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -301,22 +301,22 @@ let is_numeral symbs =
| _ ->
false
-let rec get_notation_vars = function
+let rec get_notation_vars onlyprint = function
| [] -> []
| NonTerminal id :: sl ->
- let vars = get_notation_vars sl in
+ let vars = get_notation_vars onlyprint sl in
if Id.equal id ldots_var then vars else
- if Id.List.mem id vars then
+ (* don't check for nonlinearity if printing only, see Bug 5526 *)
+ if not onlyprint && Id.List.mem id vars then
user_err ~hdr:"Metasyntax.get_notation_vars"
(str "Variable " ++ pr_id id ++ str " occurs more than once.")
- else
- id::vars
- | (Terminal _ | Break _) :: sl -> get_notation_vars sl
+ else id::vars
+ | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
| SProdList _ :: _ -> assert false
-let analyze_notation_tokens l =
+let analyze_notation_tokens ~onlyprint l =
let l = raw_analyze_notation_tokens l in
- let vars = get_notation_vars l in
+ let vars = get_notation_vars onlyprint l in
let recvars,l = interp_list_parser [] l in
recvars, List.subtract Id.equal vars (List.map snd recvars), l
@@ -1084,12 +1084,12 @@ let compute_syntax_data df modifiers =
if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
let assoc = Option.append mods.assoc (Some NonA) in
let toks = split_notation_string df in
- let recvars,mainvars,symbols = analyze_notation_tokens toks in
+ let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint toks in
let _ = check_useless_entry_types recvars mainvars mods.etyps in
let _ = check_binder_type recvars mods.etyps in
(* Notations for interp and grammar *)
-let ntn_for_interp = make_notation_key symbols in
+ let ntn_for_interp = make_notation_key symbols in
let symbols' = remove_curly_brackets symbols in
let ntn_for_grammar = make_notation_key symbols' in
if not onlyprint then check_rule_productivity symbols';
@@ -1333,7 +1333,7 @@ let add_notation_in_scope local df c mods scope =
let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
let dfs = split_notation_string df in
- let recvars,mainvars,symbs = analyze_notation_tokens dfs in
+ let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
let i_typs, onlyprint = if not (is_numeral symbs) then begin
let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in
@@ -1410,7 +1410,7 @@ let add_notation local c ((loc,df),modifiers) sc =
let add_notation_extra_printing_rule df k v =
let notk =
let dfs = split_notation_string df in
- let _,_, symbs = analyze_notation_tokens dfs in
+ let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in
make_notation_key symbs in
Notation.add_notation_extra_printing_rule notk k v
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6dee95bc5..e03e9b803 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -947,7 +947,7 @@ let rec solve_obligation prg num tac =
let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in
let _ = Pfedit.by !default_tactic in
- Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
+ Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
and obligation (user_num, name, typ) tac =
let num = pred user_num in
diff --git a/vernac/search.ml b/vernac/search.ml
index 916015800..0ff78f439 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -142,7 +142,7 @@ module ConstrPriority = struct
-(3*(num_symbols t) + size t)
let compare (_,_,_,p1) (_,_,_,p2) =
- compare p1 p2
+ Pervasives.compare p1 p2
end
module PriorityQueue = Heap.Functional(ConstrPriority)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 69492759b..d0f9c7de7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -15,7 +15,6 @@ open Flags
open Names
open Nameops
open Term
-open Pfedit
open Tacmach
open Constrintern
open Prettyp
@@ -61,35 +60,25 @@ let show_proof () =
let pprf = Proof.partial_proof p in
Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
-let show_node () =
- (* spiwack: I'm have little clue what this function used to do. I deactivated it,
- could, possibly, be cleaned away. (Feb. 2010) *)
- ()
-
-let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.")
-
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
- let pfts = get_pftreestate () in
+ let pfts = Proof_global.give_me_the_proof () in
let gls = Proof.V82.subgoals pfts in
let sigma = gls.Evd.sigma in
Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
let show_universes () =
- let pfts = get_pftreestate () in
+ let pfts = Proof_global.give_me_the_proof () in
let gls = Proof.V82.subgoals pfts in
let sigma = gls.Evd.sigma in
let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
-(* Spiwack: proof tree is currently not working *)
-let show_prooftree () = ()
-
(* Simulate the Intro(s) tactic *)
let show_intro all =
let open EConstr in
- let pf = get_pftreestate() in
+ let pf = Proof_global.give_me_the_proof() in
let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
if not (List.is_empty gls) then begin
let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
@@ -108,14 +97,29 @@ let show_intro all =
[Not_found] is raised if the given string isn't the qualid of
a known inductive type. *)
+(*
+
+ HH notes in PR #679:
+
+ The Show Match could also be made more robust, for instance in the
+ presence of let in the branch of a constructor. A
+ decompose_prod_assum would probably suffice for that, but then, it
+ is a Context.Rel.Declaration.t which needs to be matched and not
+ just a pair (name,type).
+
+ Otherwise, this is OK. After all, the API on inductive types is not
+ so canonical in general, and in this simple case, working at the
+ low-level of mind_nf_lc seems reasonable (compared to working at the
+ higher-level of Inductiveops).
+
+*)
+
let make_cases_aux glob_ref =
match glob_ref with
- | Globnames.IndRef i ->
- let {Declarations.mind_nparams = np}
- , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr }
- = Global.lookup_inductive i in
- Util.Array.fold_right2
- (fun consname typ l ->
+ | Globnames.IndRef ind ->
+ let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in
+ Util.Array.fold_right_i
+ (fun i typ l ->
let al = List.rev (fst (decompose_prod typ)) in
let al = Util.List.skipn np al in
let rec rename avoid = function
@@ -124,8 +128,9 @@ let make_cases_aux glob_ref =
let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
Id.to_string n' :: rename (n'::avoid) l in
let al' = rename [] al in
- (Id.to_string consname :: al') :: l)
- carr tarr []
+ let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
+ (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
+ tarr []
| _ -> raise Not_found
let make_cases s =
@@ -492,7 +497,7 @@ let vernac_start_proof locality p kind l lettop =
match id with
| Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
| None -> ()) l;
- if not(refining ()) then
+ if not(Proof_global.there_are_pending_proofs ()) then
if lettop then
user_err ~hdr:"Vernacentries.StartProof"
(str "Let declarations can only be used in proof editing mode.");
@@ -505,7 +510,7 @@ let vernac_end_proof ?proof = function
let vernac_exact_proof c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the begining of a proof. *)
- let status = by (Tactics.exact_proof c) in
+ let status = Pfedit.by (Tactics.exact_proof c) in
save_proof (Vernacexpr.(Proved(Opaque None,None)));
if not status then Feedback.feedback Feedback.AddedAxiom
@@ -623,8 +628,7 @@ let vernac_constraint loc poly l =
(* Modules *)
let vernac_import export refl =
- Library.import_module export (List.map qualid_of_reference refl);
- Lib.add_frozen_state ()
+ Library.import_module export (List.map qualid_of_reference refl)
let vernac_declare_module export (loc, id) binders_ast mty_ast =
(* We check the state of the system (in section, in module type)
@@ -651,7 +655,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
match mexpr_ast_l with
| [] ->
- check_no_pending_proofs ();
+ Proof_global.check_no_pending_proof ();
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
@@ -697,7 +701,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
match mty_ast_l with
| [] ->
- check_no_pending_proofs ();
+ Proof_global.check_no_pending_proof ();
let binders_ast,argsexport =
List.fold_right
(fun (export,idl,ty) (args,argsexport) ->
@@ -745,7 +749,7 @@ let vernac_include l =
(* Sections *)
let vernac_begin_section (_, id as lid) =
- check_no_pending_proofs ();
+ Proof_global.check_no_pending_proof ();
Dumpglob.dump_definition lid true "sec";
Lib.open_section id
@@ -759,7 +763,7 @@ let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set
(* Dispatcher of the "End" command *)
let vernac_end_segment (_,id as lid) =
- check_no_pending_proofs ();
+ Proof_global.check_no_pending_proof ();
match Lib.find_opening_node id with
| Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
| Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -839,14 +843,14 @@ let focus_command_cond = Proof.no_cond command_focus
there are no more goals to solve. It cannot be a tactic since
all tactics fail if there are no further goals to prove. *)
-let vernac_solve_existential = instantiate_nth_evar_com
+let vernac_solve_existential = Pfedit.instantiate_nth_evar_com
let vernac_set_end_tac tac =
let env = Genintern.empty_glob_sign (Global.env ()) in
let _, tac = Genintern.generic_intern env tac in
- if not (refining ()) then
+ if not (Proof_global.there_are_pending_proofs ()) then
user_err Pp.(str "Unknown command of the non proof-editing mode.");
- set_end_tac tac
+ Proof_global.set_endline_tactic tac
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
let vernac_set_used_variables e =
@@ -861,13 +865,13 @@ let vernac_set_used_variables e =
user_err ~hdr:"vernac_set_used_variables"
(str "Unknown variable: " ++ pr_id id))
l;
- let _, to_clear = set_used_variables l in
+ let _, to_clear = Proof_global.set_used_variables l in
let to_clear = List.map snd to_clear in
Proof_global.with_current_proof begin fun _ p ->
if List.is_empty to_clear then (p, ())
else
let tac = Tactics.clear to_clear in
- fst (solve SelectAll None tac p), ()
+ fst (Pfedit.solve SelectAll None tac p), ()
end
(*****************************)
@@ -911,12 +915,12 @@ let vernac_chdir = function
(* State management *)
let vernac_write_state file =
- Pfedit.delete_all_proofs ();
+ Proof_global.discard_all ();
let file = CUnix.make_suffix file ".coq" in
States.extern_state file
let vernac_restore_state file =
- Pfedit.delete_all_proofs ();
+ Proof_global.discard_all ();
let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
States.intern_state file
@@ -1282,7 +1286,7 @@ let _ =
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "automatic introduction of variables";
optkey = ["Automatic";"Introduction"];
optread = Flags.is_auto_intros;
@@ -1378,17 +1382,6 @@ let _ =
optread = (fun () -> !CClosure.share);
optwrite = (fun b -> CClosure.share := b) }
-(* No more undo limit in the new proof engine.
- The command still exists for compatibility (e.g. with ProofGeneral) *)
-
-let _ =
- declare_int_option
- { optdepr = true;
- optname = "the undo limit (OBSOLETE)";
- optkey = ["Undo"];
- optread = (fun _ -> None);
- optwrite = (fun _ -> ()) }
-
let _ =
declare_bool_option
{ optdepr = false;
@@ -1510,7 +1503,7 @@ let vernac_print_option key =
with Not_found -> error_undeclared_key key
let get_current_context_of_args = function
- | Some n -> get_goal_context n
+ | Some n -> Pfedit.get_goal_context n
| None -> get_current_context ()
let query_command_selector ?loc = function
@@ -1572,7 +1565,7 @@ let vernac_global_check c =
let get_nth_goal n =
- let pf = get_pftreestate() in
+ let pf = Proof_global.give_me_the_proof() in
let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
gl
@@ -1761,7 +1754,7 @@ let vernac_locate = let open Feedback in function
| LocateFile f -> msg_notice (locate_file f)
let vernac_register id r =
- if Pfedit.refining () then
+ if Proof_global.there_are_pending_proofs () then
user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
let kn = Constrintern.global_reference (snd id) in
if not (isConstRef kn) then
@@ -1828,24 +1821,16 @@ let vernac_show = let open Feedback in function
| GoalUid id -> pr_goal_by_uid id
in
msg_notice info
- | ShowGoalImplicitly None ->
- Constrextern.with_implicits msg_notice (pr_open_subgoals ())
- | ShowGoalImplicitly (Some n) ->
- Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n)
| ShowProof -> show_proof ()
- | ShowNode -> show_node ()
| ShowExistentials -> show_top_evars ()
| ShowUniverses -> show_universes ()
- | ShowTree -> show_prooftree ()
| ShowProofNames ->
- msg_notice (pr_sequence pr_id (Pfedit.get_all_proof_names()))
+ msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names()))
| ShowIntros all -> show_intro all
| ShowMatch id -> show_match id
- | ShowThesis -> show_thesis ()
-
let vernac_check_guard () =
- let pts = get_pftreestate () in
+ let pts = Proof_global.give_me_the_proof () in
let pfterm = List.hd (Proof.partial_proof pts) in
let message =
try
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 18:11:23 +0000