aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml2
-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/obligations.ml2
-rw-r--r--vernac/vernacentries.ml77
8 files changed, 42 insertions, 82 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8e6a0f6a72..aba61146c7 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;
]
diff --git a/vernac/command.ml b/vernac/command.ml
index b1425d7034..998e7803e1 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 9bbc2fdac1..2a52d9bcb5 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 c2c27eb78e..44d6f37cc6 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 77e356eb2c..5bf419caf5 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 d06b8fd14b..a9c0d99f30 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/obligations.ml b/vernac/obligations.ml
index 6dee95bc54..e03e9b8039 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/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b75..d0f9c7de74 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
@@ -508,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.");
@@ -521,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
@@ -639,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)
@@ -667,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) ->
@@ -713,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) ->
@@ -761,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
@@ -775,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
@@ -855,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 =
@@ -877,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
(*****************************)
@@ -927,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
@@ -1298,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;
@@ -1394,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;
@@ -1526,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
@@ -1588,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
@@ -1777,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
@@ -1844,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.25.1) at 2026-04-30 14:38:42 +0000