aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/decl_mode/decl_mode.ml6
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--plugins/funind/recdef.ml18
-rw-r--r--proofs/monads.ml117
-rw-r--r--proofs/pfedit.ml20
-rw-r--r--proofs/pfedit.mli15
-rw-r--r--proofs/proof.ml4
-rw-r--r--proofs/proof.mli4
-rw-r--r--proofs/proof_global.ml8
-rw-r--r--proofs/proof_global.mli7
-rw-r--r--proofs/proofview.ml124
-rw-r--r--proofs/proofview.mli10
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/g_rewrite.ml415
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/rewrite.ml9
-rw-r--r--tactics/rewrite.mli2
-rw-r--r--tactics/tactics.ml7
-rw-r--r--toplevel/auto_ind_decl.ml12
-rw-r--r--toplevel/classes.ml7
-rw-r--r--toplevel/obligations.ml5
-rw-r--r--toplevel/vernacentries.ml26
25 files changed, 293 insertions, 145 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index f3c5da2ad..cbdcc96aa 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -100,13 +100,13 @@ let proof_cond = Proof.no_cond proof_focus
let focus p =
let inf = get_stack p in
- Proof_global.with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
+ Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
let unfocus () =
- Proof_global.with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
+ Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
let maximal_unfocus () =
- Proof_global.with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
+ Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
let get_top_stack pts =
try
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e47776bd7..6b5cb7492 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -121,7 +121,7 @@ let start_proof_tac gls=
tcl_change_info info gls
let go_to_proof_mode () =
- Pfedit.by (Proofview.V82.tactic start_proof_tac);
+ ignore (Pfedit.by (Proofview.V82.tactic start_proof_tac));
let p = Proof_global.give_me_the_proof () in
Decl_mode.focus p
@@ -1461,7 +1461,7 @@ let do_instr raw_instr pts =
let glob_instr = intern_proof_instr ist raw_instr in
let instr =
interp_proof_instr (get_its_info gl) sigma env glob_instr in
- Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))
+ ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)))
else () end;
postprocess pts raw_instr.instr;
(* spiwack: this should restore a compatible semantics with
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2da4b6147..8c2fdb7eb 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
lemma_type
(fun _ _ -> ());
- Pfedit.by (Proofview.V82.tactic prove_replacement);
+ ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
Lemmas.save_named false
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 0850d556c..3d577b440 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -297,7 +297,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
(hook new_principle_type)
;
(* let _tim1 = System.get_time () in *)
- Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams));
+ ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map mkConst funs) mutr_nparams)));
(* let _tim2 = System.get_time () in *)
(* begin *)
(* let dur1 = System.time_difference tim1 tim2 in *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ce25f7aaf..36de85595 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1069,9 +1069,9 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i))
(fun _ _ -> ());
- Pfedit.by
+ ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
- (proving_tac i)));
+ (proving_tac i))));
do_save ();
let finfo = find_Function_infos f_as_constant in
let lem_cst = destConst (Constrintern.global_reference lem_id) in
@@ -1120,9 +1120,9 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
(Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
(fst lemmas_types_infos.(i))
(fun _ _ -> ());
- Pfedit.by
+ ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
- (proving_tac i)));
+ (proving_tac i))));
do_save ();
let finfo = find_Function_infos f_as_constant in
let lem_cst = destConst (Constrintern.global_reference lem_id) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 76095cb1c..881d930fc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1319,10 +1319,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
hook;
if Indfun_common.is_strict_tcc ()
then
- by (Proofview.V82.tactic (tclIDTAC))
+ ignore (by (Proofview.V82.tactic (tclIDTAC)))
else
begin
- by (Proofview.V82.tactic begin
+ ignore (by (Proofview.V82.tactic begin
fun g ->
tclTHEN
(decompose_and_tac)
@@ -1338,10 +1338,10 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
)
using_lemmas)
) tclIDTAC)
- g end)
+ g end))
end;
try
- by (Proofview.V82.tactic tclIDTAC); (* raises UserError _ if the proof is complete *)
+ ignore (by (Proofview.V82.tactic tclIDTAC)); (* raises UserError _ if the proof is complete *)
with UserError _ ->
defined ()
@@ -1364,9 +1364,9 @@ let com_terminate
(Global, Proof Lemma) (Environ.named_context_val env)
(compute_terminate_type nb_args fonctional_ref) hook;
- by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start));
- by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
- input_type relation rec_arg_num )))
+ ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
+ ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
+ input_type relation rec_arg_num ))))
in
start_proof tclIDTAC tclIDTAC;
try
@@ -1410,7 +1410,7 @@ let (com_eqn : int -> Id.t ->
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(start_proof eq_name (Global, Proof Lemma)
(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
- by
+ ignore (by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
(fun x ->
prove_eq (fun _ -> tclIDTAC)
@@ -1437,7 +1437,7 @@ let (com_eqn : int -> Id.t ->
ih = Id.of_string "______";
}
)
- ));
+ )));
(* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
Flags.silently (fun () -> Lemmas.save_named opacity) () ;
diff --git a/proofs/monads.ml b/proofs/monads.ml
index ba1440864..803715a45 100644
--- a/proofs/monads.ml
+++ b/proofs/monads.ml
@@ -22,6 +22,13 @@ module type State = sig
val get : s t
end
+module type Writer = sig
+ type m (* type of the messages *)
+ include S
+
+ val put : m -> unit t
+end
+
module type IO = sig
include S
@@ -133,6 +140,54 @@ end = struct
T.return { result=s ; state=s }
end
+module type Monoid = sig
+ type t
+
+ val zero : t
+ val ( * ) : t -> t -> t
+end
+
+module Writer (M:Monoid) (T:S) : sig
+ include Writer with type +'a t = private ('a*M.t) T.t and type m = M.t
+
+ val lift : 'a T.t -> 'a t
+ (* The coercion from private ['a t] in function form. *)
+ val run : 'a t -> ('a*m) T.t
+end = struct
+
+ type 'a t = ('a*M.t) T.t
+ type m = M.t
+
+ let run x = x
+
+ (*spiwack: convenience notation, waiting for ocaml 3.12 *)
+ let (>>=) = T.bind
+
+ let bind x k =
+ x >>= fun (a,m) ->
+ k a >>= fun (r,m') ->
+ T.return (r,M.( * ) m m')
+
+ let seq x k =
+ x >>= fun ((),m) ->
+ k >>= fun (r,m') ->
+ T.return (r,M.( * ) m m')
+
+ let return x =
+ T.return (x,M.zero)
+
+ let ignore x =
+ x >>= fun (_,m) ->
+ T.return ((),m)
+
+ let lift x =
+ x >>= fun r ->
+ T.return (r,M.zero)
+
+ let put m =
+ T.return ((),m)
+end
+
(* Double-continuation backtracking monads are reasonable folklore for
"search" implementations (including Tac interactive prover's
tactics). Yet it's quite hard to wrap your head around these. I
@@ -301,6 +356,7 @@ module StateLogic(X:Type)(T:Logic) : sig
val set : s -> unit t
val get : s t
+ val lift : 'a T.t -> 'a t
val run : 'a t -> s -> 'a result T.t
end = struct
@@ -370,14 +426,71 @@ end = struct
return a.result
end
+(* [Writer(M)(T:Logic)] can be lifted to [Logic] by backtracking on state on [plus].*)
+module WriterLogic(M:Monoid)(T:Logic) : sig
+ (* spiwack: some duplication from interfaces as we need ocaml 3.12
+ to substitute inside signatures. *)
+ type m = M.t
+ include Logic with type +'a t = private ('a*m) T.t
+ val put : m -> unit t
+ val lift : 'a T.t -> 'a t
+ val run : 'a t -> ('a*m) T.t
+end = struct
+ module W = Writer(M)(T)
+ include W
+ let zero e = lift (T.zero e)
+ let plus x y =
+ (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+ let (>>=) = bind in
+ let (>>) = seq in
+ lift begin
+ (T.plus (run x) (fun e -> run (y e)))
+ end >>= fun (r,m) ->
+ put m >>
+ return r
+ let split x =
+ (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+ let (>>=) = bind in
+ let (>>) = seq in
+ lift (T.split (run x)) >>= function
+ | Util.Inr _ as e -> return e
+ | Util.Inl ((a,m),y) ->
+ let y' e =
+ lift (y e) >>= fun (b,m) ->
+ put m >>
+ return b
+ in
+ put m >>
+ return (Util.Inl(a,y'))
+ (*** IO ***)
+ type 'a ref = 'a T.ref
+ let ref x = lift (T.ref x)
+ let (:=) r x = lift (T.(:=) r x)
+ let (!) r = lift (T.(!) r)
+ let raise e = lift (T.raise e)
+ let catch t h =
+ (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+ let (>>=) = bind in
+ let (>>) = seq in
+ let h' e = run (h e) in
+ lift (T.catch (run t) h') >>= fun (a,m) ->
+ put m >>
+ return a
-
-
+ exception Timeout
+ let timeout n t =
+ (* spiwack: convenience notation, waiting for ocaml 3.12 *)
+ let (>>=) = bind in
+ let (>>) = seq in
+ lift (T.timeout n (run t)) >>= fun (a,m) ->
+ put m >>
+ return a
+end
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 55c46a340..6c0ddfc11 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -33,10 +33,10 @@ let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook =
let goals = [ (Global.env_of_context hyps , c) ] in
Proof_global.start_proof id str goals ?compute_guard hook;
let env = Global.env () in
- Proof_global.with_current_proof (fun _ p ->
+ ignore (Proof_global.with_current_proof (fun _ p ->
match init_tac with
- | None -> p
- | Some tac -> Proof.run_tactic env tac p)
+ | None -> p,true
+ | Some tac -> Proof.run_tactic env tac p))
let cook_this_proof hook p =
match p with
@@ -105,7 +105,7 @@ let solve_nth ?with_end_tac gi tac pr =
let by tac = Proof_global.with_current_proof (fun _ -> solve_nth 1 tac)
let instantiate_nth_evar_com n com =
- Proof_global.with_current_proof (fun _ -> Proof.V82.instantiate_evar n com)
+ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p)
(**********************************************************************)
@@ -118,10 +118,10 @@ let next = let n = ref 0 in fun () -> incr n; !n
let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
start_proof id goal_kind sign typ (fun _ _ -> ());
try
- by tac;
+ let status = by tac in
let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
delete_current_proof ();
- const
+ const, status
with reraise ->
delete_current_proof ();
raise reraise
@@ -134,11 +134,11 @@ let constr_of_def = function
let build_by_tactic env typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
- let ce = build_constant_by_tactic id sign typ tac in
+ let ce,status = build_constant_by_tactic id sign typ tac in
let ce = Term_typing.handle_side_effects env ce in
let cb, se = Future.force ce.const_entry_body in
- assert(Declareops.side_effects_is_empty se);
- cb
+ assert(Declareops.side_effects_is_empty (Declareops.no_seff));
+ cb,status
(**********************************************************************)
(* Support for resolution of evars in tactic interpretation, including
@@ -155,7 +155,7 @@ let solve_by_implicit_tactic env sigma evk =
when
Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
- (try build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []))
+ (try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) [])))
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 3a0c25c46..73f12db98 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -136,13 +136,14 @@ val get_used_variables : unit -> Context.section_context option
if there is no [n]th subgoal *)
val solve_nth : ?with_end_tac:unit Proofview.tactic -> int -> unit Proofview.tactic ->
- Proof.proof -> Proof.proof
+ Proof.proof -> Proof.proof*bool
(** [by tac] applies tactic [tac] to the 1st subgoal of the current
focused proof or raises a UserError if there is no focused proof or
- if there is no more subgoals *)
+ if there is no more subgoals.
+ Returns [false] if an unsafe tactic has been used. *)
-val by : unit Proofview.tactic -> unit
+val by : unit Proofview.tactic -> bool
(** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
existential variable of the current focused proof by [c] or raises a
@@ -151,12 +152,14 @@ val by : unit Proofview.tactic -> unit
val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
-(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
+(** [build_by_tactic typ tac] returns a term of type [typ] by calling
+ [tac]. The return boolean, if [false] indicates the use of an unsafe
+ tactic. *)
val build_constant_by_tactic :
Id.t -> named_context_val -> ?goal_kind:goal_kind ->
- types -> unit Proofview.tactic -> Entries.definition_entry
-val build_by_tactic : env -> types -> unit Proofview.tactic -> constr
+ types -> unit Proofview.tactic -> Entries.definition_entry * bool
+val build_by_tactic : env -> types -> unit Proofview.tactic -> constr * bool
(** Declare the default tactic to fill implicit arguments *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 89f3638a1..3a00d76f0 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -252,8 +252,8 @@ let initial_goals p = Proofview.initial_goals p.proofview
let run_tactic env tac pr =
let sp = pr.proofview in
- let (_,tacticced_proofview) = Proofview.apply env tac sp in
- { pr with proofview = tacticced_proofview }
+ let (_,tacticced_proofview,status) = Proofview.apply env tac sp in
+ { pr with proofview = tacticced_proofview },status
let emit_side_effects eff pr =
{pr with proofview = Proofview.emit_side_effects eff pr.proofview}
diff --git a/proofs/proof.mli b/proofs/proof.mli
index fa6007061..66aee0313 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -128,7 +128,9 @@ val no_focused_goal : proof -> bool
(*** Tactics ***)
-val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof
+(* the returned boolean signal whether an unsafe tactic has been
+ used. In which case it is [false]. *)
+val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof*bool
val emit_side_effects : Declareops.side_effects -> proof -> proof
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3f84f6500..5e11cfdb2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -154,8 +154,12 @@ let with_current_proof f =
match p.endline_tactic with
| None -> Proofview.tclUNIT ()
| Some tac -> !interp_tac tac in
- let p = { p with proof = f et p.proof } in
- pstates := p :: rest
+ let (newpr,status) = f et p.proof in
+ let p = { p with proof = newpr } in
+ pstates := p :: rest;
+ status
+let simple_with_current_proof f =
+ ignore (with_current_proof (fun t p -> f t p , true))
(* Sets the tactic to be used when a tactic line is closed with [...] *)
let set_endline_tactic tac =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 9b5015e0c..867010fb0 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -79,9 +79,12 @@ exception NoSuchProof
val get_open_goals : unit -> int
-(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
- no current proof. *)
+(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
+ no current proof.
+ The return boolean is set to [false] if an unsafe tactic has been used. *)
val with_current_proof :
+ (unit Proofview.tactic -> Proof.proof -> Proof.proof*bool) -> bool
+val simple_with_current_proof :
(unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
(** Sets the tactic to be used when a tactic line is closed with [...] *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 3f80da785..a3791e7a4 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -190,81 +190,88 @@ let unfocus c sp =
- backtrack on previous changes of the proofview *)
(* spiwack: it seems lighter, for now, to deal with the environment here rather than in [Monads]. *)
-module LocalState = struct
+module ProofState = struct
type t = proofview
end
+module MessageType = struct
+ type t = bool (* [false] if an unsafe tactic has been used. *)
+
+ let zero = true
+ let ( * ) s1 s2 = s1 && s2
+end
module Backtrack = Monads.Logic(Monads.IO)
-module Inner = Monads.StateLogic(LocalState)(Backtrack)
+module Message = Monads.WriterLogic(MessageType)(Backtrack)
+module Proof = Monads.StateLogic(ProofState)(Message)
-type +'a tactic = Environ.env -> 'a Inner.t
+type +'a tactic = Environ.env -> 'a Proof.t
(* Applies a tactic to the current proofview. *)
let apply env t sp =
- let next = Monads.IO.run (Backtrack.run (Inner.run (t env) sp)) in
- next.Inner.result , next.Inner.state
+ let (next,status) = Monads.IO.run (Backtrack.run (Message.run (Proof.run (t env) sp))) in
+ next.Proof.result , next.Proof.state , status
(*** tacticals ***)
(* Unit of the tactic monad *)
-let tclUNIT a _ = Inner.return a
+let tclUNIT a _ = Proof.return a
(* Bind operation of the tactic monad *)
let tclBIND t k env =
- Inner.bind (t env) (fun a -> k a env)
+ Proof.bind (t env) (fun a -> k a env)
(* Interpretes the ";" (semicolon) of Ltac.
As a monadic operation, it's a specialized "bind"
on unit-returning tactic (meaning "there is no value to bind") *)
let tclTHEN t1 t2 env =
- Inner.seq (t1 env) (t2 env)
+ Proof.seq (t1 env) (t2 env)
(* [tclIGNORE t] has the same operational content as [t],
but drops the value at the end. *)
-let tclIGNORE tac env = Inner.ignore (tac env)
+let tclIGNORE tac env = Proof.ignore (tac env)
(* [tclOR t1 t2 = t1] as long as [t1] succeeds. Whenever the successes
of [t1] have been depleted and it failed with [e], then it behaves
as [t2 e]. No interleaving at this point. *)
let tclOR t1 t2 env =
- Inner.plus (t1 env) (fun e -> t2 e env)
+ Proof.plus (t1 env) (fun e -> t2 e env)
(* [tclZERO e] always fails with error message [e]*)
-let tclZERO e _ = Inner.zero e
+let tclZERO e _ = Proof.zero e
(* [tclORELSE t1 t2] behaves like [t1] if [t1] succeeds at least once
or [t2] if [t1] fails. *)
let tclORELSE t1 t2 env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- Inner.split (t1 env) >>= function
+ let (>>=) = Proof.bind in
+ Proof.split (t1 env) >>= function
| Util.Inr e -> t2 e env
- | Util.Inl (a,t1') -> Inner.plus (Inner.return a) t1'
+ | Util.Inl (a,t1') -> Proof.plus (Proof.return a) t1'
(* [tclIFCATCH a s f] is a generalisation of [tclORELSE]: if [a]
succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a]
fails with [e], then it behaves as [f e]. *)
let tclIFCATCH a s f env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- Inner.split (a env) >>= function
+ let (>>=) = Proof.bind in
+ Proof.split (a env) >>= function
| Util.Inr e -> f e env
- | Util.Inl (x,a') -> Inner.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env))
+ | Util.Inl (x,a') -> Proof.plus (s x env) (fun e -> (a' e) >>= fun x' -> (s x' env))
(* Focuses a tactic at a range of subgoals, found by their indices. *)
(* arnaud: bug if 0 goals ! *)
let tclFOCUS i j t env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- let (>>) = Inner.seq in
- Inner.get >>= fun initial ->
+ let (>>=) = Proof.bind in
+ let (>>) = Proof.seq in
+ Proof.get >>= fun initial ->
try
let (focused,context) = focus i j initial in
- Inner.set focused >>
+ Proof.set focused >>
t (env) >>= fun result ->
- Inner.get >>= fun next ->
- Inner.set (unfocus context next) >>
- Inner.return result
+ Proof.get >>= fun next ->
+ Proof.set (unfocus context next) >>
+ Proof.return result
with e ->
(* spiwack: a priori the only possible exceptions are that of focus,
of course I haven't made them algebraic yet. *)
@@ -294,24 +301,24 @@ end
let rec tclDISPATCHGEN null join tacs env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- let (>>) = Inner.seq in
- Inner.get >>= fun initial ->
+ let (>>=) = Proof.bind in
+ let (>>) = Proof.seq in
+ Proof.get >>= fun initial ->
match tacs,initial.comb with
| [], [] -> tclUNIT null env
| t::tacs , first::goals ->
begin match Goal.advance initial.solution first with
- | None -> Inner.return null (* If [first] has been solved by side effect: do nothing. *)
+ | None -> Proof.return null (* If [first] has been solved by side effect: do nothing. *)
| Some first ->
- Inner.set {initial with comb=[first]} >>
+ Proof.set {initial with comb=[first]} >>
t env
end >>= fun y ->
- Inner.get >>= fun step ->
- Inner.set {step with comb=goals} >>
+ Proof.get >>= fun step ->
+ Proof.set {step with comb=goals} >>
tclDISPATCHGEN null join tacs env >>= fun x ->
- Inner.get >>= fun step' ->
- Inner.set {step' with comb=step.comb@step'.comb} >>
- Inner.return (join y x)
+ Proof.get >>= fun step' ->
+ Proof.set {step' with comb=step.comb@step'.comb} >>
+ Proof.return (join y x)
| _ , _ -> tclZERO SizeMismatch env
let unitK () () = ()
@@ -338,8 +345,8 @@ let extend_to_list =
startxs@(copy (n-ne-ns) rx endxs)
let tclEXTEND tacs1 rtac tacs2 env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- Inner.get >>= fun step ->
+ let (>>=) = Proof.bind in
+ Proof.get >>= fun step ->
let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
tclDISPATCH tacs env
@@ -362,20 +369,20 @@ let sensitive_on_proofview s env step =
comb = List.flatten combed_subgoals; }
let tclSENSITIVE s env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- Inner.get >>= fun step ->
+ let (>>=) = Proof.bind in
+ Proof.get >>= fun step ->
try
let next = sensitive_on_proofview s env step in
- Inner.set next
+ Proof.set next
with e when Errors.noncritical e ->
tclZERO e env
let tclPROGRESS t env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- Inner.get >>= fun initial ->
+ let (>>=) = Proof.bind in
+ Proof.get >>= fun initial ->
t env >>= fun res ->
- Inner.get >>= fun final ->
+ Proof.get >>= fun final ->
let test =
Evd.progress_evar_map initial.solution final.solution &&
not (Util.List.for_all2eq (fun i f -> Goal.equal initial.solution i final.solution f) initial.comb final.comb)
@@ -387,14 +394,17 @@ let tclPROGRESS t env =
let tclEVARMAP _ =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- Inner.get >>= fun initial ->
- Inner.return (initial.solution)
+ let (>>=) = Proof.bind in
+ Proof.get >>= fun initial ->
+ Proof.return (initial.solution)
let tclENV env =
- Inner.return env
+ Proof.return env
+
+let tclTIMEOUT n t env = Proof.timeout n (t env)
-let tclTIMEOUT n t env = Inner.timeout n (t env)
+let mark_as_unsafe env =
+ Proof.lift (Message.put false)
(*** Commands ***)
@@ -450,8 +460,8 @@ module V82 = struct
(* spiwack: we ignore the dependencies between goals here, expectingly
preserving the semantics of <= 8.2 tactics *)
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- Inner.get >>= fun ps ->
+ let (>>=) = Proof.bind in
+ Proof.get >>= fun ps ->
try
let tac evd gl =
let glsigma =
@@ -466,7 +476,7 @@ module V82 = struct
in
let (goalss,evd) = Goal.list_map tac initgoals initevd in
let sgs = List.flatten goalss in
- Inner.set { ps with solution=evd ; comb=sgs; }
+ Proof.set { ps with solution=evd ; comb=sgs; }
with e when Errors.noncritical e ->
tclZERO e env
@@ -516,9 +526,11 @@ module V82 = struct
let of_tactic t gls =
let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
- let (_,final) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
+ let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
{ Evd.sigma = final.solution ; it = final.comb }
+ let put_status b _env =
+ Proof.lift (Message.put b)
end
@@ -528,17 +540,17 @@ module Goal = struct
let lift s env =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Inner.bind in
- let (>>) = Inner.seq in
- Inner.get >>= fun step ->
+ let (>>=) = Proof.bind in
+ let (>>) = Proof.seq in
+ Proof.get >>= fun step ->
try
let (res,sigma) =
Goal.list_map begin fun sigma g ->
Goal.eval s env sigma g
end step.comb step.solution
in
- Inner.set { step with solution=sigma } >>
- Inner.return res
+ Proof.set { step with solution=sigma } >>
+ Proof.return res
with e when Errors.noncritical e ->
tclZERO e env
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index d2db5be9a..4536180e2 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -118,7 +118,9 @@ val unfocus : focus_context -> proofview -> proofview
type +'a tactic
(* Applies a tactic to the current proofview. *)
-val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview
+(* the return boolean signals the use of an unsafe tactic, in which
+ case it is [false]. *)
+val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview * bool
(*** tacticals ***)
@@ -198,6 +200,9 @@ val tclENV : Environ.env tactic
In case of timeout if fails with [tclZERO Timeout]. *)
val tclTIMEOUT : int -> 'a tactic -> 'a tactic
+(** [mark_as_unsafe] signals that the current tactic is unsafe. *)
+val mark_as_unsafe : unit tactic
+
val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
(*** Commands ***)
@@ -260,6 +265,9 @@ module V82 : sig
should be avoided as much as possible. It should work as
expected for a tactic obtained from {!V82.tactic} though. *)
val of_tactic : 'a tactic -> tac
+
+ (* marks as unsafe if the argument is [false] *)
+ val put_status : bool -> unit tactic
end
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a383b1452..9edf6302d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -785,5 +785,5 @@ END;;
VERNAC COMMAND EXTEND GrabEvars
[ "Grab" "Existential" "Variables" ]
=> [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ]
- -> [ Proof_global.with_current_proof (fun _ p -> Proof.V82.grab_evars p) ]
+ -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ]
END
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index f889f9cb2..846bba1d4 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -146,21 +146,20 @@ TACTIC EXTEND setoid_rewrite
[ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))]
END
-let cl_rewrite_clause_newtac_tac c o occ cl gl =
- cl_rewrite_clause_newtac' c o occ cl;
- tclIDTAC gl
+let cl_rewrite_clause_newtac_tac c o occ cl =
+ cl_rewrite_clause_newtac' c o occ cl
TACTIC EXTEND GenRew
| [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] ->
- [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id)) ]
+ [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
| [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] ->
- [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id)) ]
+ [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
| [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
- [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id)) ]
+ [ cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id) ]
| [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
- [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None) ]
+ [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ]
| [ "rew" orient(o) glob_constr_with_bindings(c) ] ->
- [ Proofview.V82.tactic (cl_rewrite_clause_newtac_tac c o AllOccurrences None) ]
+ [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ]
END
VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 06b067fcf..04819830e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -198,8 +198,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
*)
let pf = Proof.start [invEnv,invGoal] in
let pf =
- Proof.run_tactic env (
- Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf
+ fst (Proof.run_tactic env (
+ Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf)
in
let pfterm = List.hd (Proof.partial_proof pf) in
let global_named_context = Global.named_context () in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 30fe8d4ae..66b2c64b0 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -361,7 +361,7 @@ let solve_remaining_by by env prf =
let evd' =
List.fold_right (fun mv evd ->
let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
- let c = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in
+ let c,_ = Pfedit.build_by_tactic env.env ty (Tacticals.New.tclCOMPLETE tac) in
meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
indep env.evd
in { env with evd = evd' }, prf
@@ -1342,9 +1342,8 @@ let cl_rewrite_clause_new_strat ?abs strat clause =
newfail 0 (str"setoid rewrite failed: " ++ s))
let cl_rewrite_clause_newtac' l left2right occs clause =
- Proof_global.with_current_proof (fun _ -> Proof.run_tactic (Global.env ())
- (Proofview.tclFOCUS 1 1
- (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)))
+ Proofview.tclFOCUS 1 1
+ (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)
let cl_rewrite_clause_strat strat clause =
tclTHEN (tactic_init_setoid ())
@@ -1641,7 +1640,7 @@ let add_morphism_infer glob m n =
glob (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false);
- Pfedit.by (Tacinterp.interp tac)) ()
+ ignore (Pfedit.by (Tacinterp.interp tac))) ()
let add_morphism glob binders m s n =
init_setoid ();
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 637bab5a6..63166c64a 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -43,7 +43,7 @@ val cl_rewrite_clause :
val cl_rewrite_clause_newtac' :
interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) ->
- bool -> Locus.occurrences -> Id.t option -> unit
+ bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic
val is_applied_rewrite_relation :
env -> evar_map -> Context.rel_context -> constr -> types option
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5b1ae69e3..4026b4258 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3740,7 +3740,8 @@ let abstract_subproof id tac gl =
try flush_and_check_evars (project gl) concl
with Uninstantiated_evar _ ->
error "\"abstract\" cannot handle existentials." in
- let const = Pfedit.build_constant_by_tactic id secsign concl
+ (* spiwack: the [abstract] tacticals loses the "unsafe status" information *)
+ let (const,_) = Pfedit.build_constant_by_tactic id secsign concl
(Tacticals.New.tclCOMPLETE (Tacticals.New.tclTHEN (Tacticals.New.tclDO (List.length sign) intro) tac)) in
let cd = Entries.DefinitionEntry const in
let decl = (cd, IsProof Lemma) in
@@ -3764,9 +3765,9 @@ let tclABSTRACT name_op tac gl =
let admit_as_an_axiom =
- (* spiwack: admit temporarily won't report an unsafe status *)
Proofview.tclUNIT () >= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
- simplest_case (Coqlib.build_coq_proof_admitted ())
+ simplest_case (Coqlib.build_coq_proof_admitted ()) <*>
+ Proofview.mark_as_unsafe
let unify ?(state=full_transparent_state) x y gl =
try
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f35a34633..50d013044 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -626,8 +626,8 @@ let make_bl_scheme mind =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
- [|Pfedit.build_by_tactic (Global.env()) bl_goal
- (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|],
+ [|fst (Pfedit.build_by_tactic (Global.env()) bl_goal
+ (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec))|],
eff
let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
@@ -741,8 +741,8 @@ let make_lb_scheme mind =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
- [|Pfedit.build_by_tactic (Global.env()) lb_goal
- (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|],
+ [|fst (Pfedit.build_by_tactic (Global.env()) lb_goal
+ (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec))|],
eff
let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
@@ -903,9 +903,9 @@ let make_eq_decidability mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|Pfedit.build_by_tactic (Global.env())
+ [|fst (Pfedit.build_by_tactic (Global.env())
(compute_dec_goal ind lnamesparrec nparrec)
- (compute_dec_tact ind lnamesparrec nparrec)|], Declareops.no_seff
+ (compute_dec_tact ind lnamesparrec nparrec))|], Declareops.no_seff
let eq_dec_scheme_kind =
declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 121f8f4e1..728baadb4 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -298,11 +298,12 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
(fun () ->
Lemmas.start_proof id kind termtype
(fun _ -> instance_hook k pri global imps ?hook);
+ (* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
- Pfedit.by (!refine_ref (evm, Option.get term))
+ ignore (Pfedit.by (!refine_ref (evm, Option.get term)))
else if Flags.is_auto_intros () then
- Pfedit.by (Tacticals.New.tclDO len Tactics.intro);
- (match tac with Some tac -> Pfedit.by tac | None -> ())) ();
+ ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
+ (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
id)
end)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 13e12b7e1..3eb61ccdf 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -761,7 +761,8 @@ let rec string_of_list sep f = function
(* Solve an obligation using tactics, return the corresponding proof term *)
let solve_by_tac evi t =
let id = Id.of_string "H" in
- let entry = Pfedit.build_constant_by_tactic
+ (* spiwack: the status is dropped *)
+ let (entry,_) = Pfedit.build_constant_by_tactic
id ~goal_kind evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
let env = Global.env () in
let entry = Term_typing.handle_side_effects env entry in
@@ -814,7 +815,7 @@ let rec solve_obligation prg num tac =
| _ -> ());
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
Printer.pr_constr_env (Global.env ()) obl.obl_type);
- Pfedit.by (snd (get_default_tactic ()));
+ ignore (Pfedit.by (snd (get_default_tactic ())));
Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a0a355a15..62243781a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -475,8 +475,9 @@ 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. *)
- by (Tactics.New.exact_proof c);
- save_named true
+ let status = by (Tactics.New.exact_proof c) in
+ save_named true;
+ if not status then Pp.feedback Interface.AddedAxiom
let vernac_assumption locality (local, kind) l nl =
let local = enforce_locality_exp locality local in
@@ -774,15 +775,16 @@ let focus_command_cond = Proof.no_cond command_focus
let vernac_solve n tcom b =
if not (refining ()) then
error "Unknown command of the non proof-editing mode.";
- Proof_global.with_current_proof (fun etac p ->
+ let status = Proof_global.with_current_proof (fun etac p ->
let with_end_tac = if b then Some etac else None in
- let p = solve_nth n (Tacinterp.hide_interp tcom None) ?with_end_tac p in
+ let (p,status) = solve_nth n (Tacinterp.hide_interp tcom None) ?with_end_tac p in
(* in case a strict subtree was completed,
go back to the top of the prooftree *)
let p = Proof.maximal_unfocus command_focus p in
- p);
- print_subgoals()
-;;
+ p,status) in
+ print_subgoals();
+ if not status then Pp.feedback Interface.AddedAxiom
+
(* A command which should be a tactic. It has been
added by Christine to patch an error in the design of the proof
@@ -1486,7 +1488,7 @@ let vernac_register id r =
(* Proof management *)
let vernac_focus gln =
- Proof_global.with_current_proof (fun _ p ->
+ Proof_global.simple_with_current_proof (fun _ p ->
match gln with
| None -> Proof.focus focus_command_cond () 1 p
| Some 0 ->
@@ -1497,7 +1499,7 @@ let vernac_focus gln =
(* Unfocuses one step in the focus stack. *)
let vernac_unfocus () =
- Proof_global.with_current_proof (fun _ p -> Proof.unfocus command_focus p ());
+ Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus command_focus p ());
print_subgoals ()
(* Checks that a proof is fully unfocused. Raises an error if not. *)
@@ -1519,19 +1521,19 @@ let subproof_kind = Proof.new_focus_kind ()
let subproof_cond = Proof.done_cond subproof_kind
let vernac_subproof gln =
- Proof_global.with_current_proof (fun _ p ->
+ Proof_global.simple_with_current_proof (fun _ p ->
match gln with
| None -> Proof.focus subproof_cond () 1 p
| Some n -> Proof.focus subproof_cond () n p);
print_subgoals ()
let vernac_end_subproof () =
- Proof_global.with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ());
+ Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus subproof_kind p ());
print_subgoals ()
let vernac_bullet (bullet:Proof_global.Bullet.t) =
- Proof_global.with_current_proof (fun _ p ->
+ Proof_global.simple_with_current_proof (fun _ p ->
Proof_global.Bullet.put p bullet);
(* Makes the focus visible in emacs by re-printing the goal. *)
if !Flags.print_emacs then print_subgoals ()
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 11:32:52 +0000