aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof_type.ml8
-rw-r--r--proofs/proof_type.mli5
-rw-r--r--proofs/refiner.ml11
-rw-r--r--proofs/refiner.mli9
4 files changed, 15 insertions, 18 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 403723702..5c9d2406e 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -40,12 +40,6 @@ type prim_rule =
| Move of bool * identifier * identifier
| Rename of identifier * identifier
-(*s Proof trees.
- [ref] = [None] if the goal has still to be proved,
- and [Some (r,l)] if the rule [r] was applied to the goal
- and gave [l] as subproofs to be completed.
- if [ref = (Some(Tactic (t,p),l))] then [p] is the proof
- that the goal can be proven if the goals in [l] are solved. *)
type proof_tree = {
open_subgoals : int;
goal : goal;
@@ -59,7 +53,7 @@ and rule =
| Change_evars
and compound_rule=
- | Tactic of tactic_expr
+ | Tactic of tactic_expr * bool
| Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
and goal = evar_info
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 74c36c981..9c82239ef 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -72,7 +72,7 @@ type prim_rule =
[ref] = [None] if the goal has still to be proved,
and [Some (r,l)] if the rule [r] was applied to the goal
and gave [l] as subproofs to be completed.
- if [ref = (Some(Tactic (t,p),l))] then [p] is the proof
+ if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof
that the goal can be proven if the goals in [l] are solved. *)
type proof_tree = {
open_subgoals : int;
@@ -87,7 +87,8 @@ and rule =
| Change_evars
and compound_rule=
- | Tactic of tactic_expr
+ (* the boolean of Tactic tells if the default tactic is used *)
+ | Tactic of tactic_expr * bool
| Proof_instr of bool * proof_instr
and goal = evar_info
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3d65406b8..2c02fb6f1 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -173,13 +173,14 @@ let abstract_operation syntax semantics gls =
goal = gls.it;
ref = Some(Nested(syntax,hidden_proof),spfl)})
-let abstract_tactic_expr te tacfun gls =
- abstract_operation (Tactic te) tacfun gls
+let abstract_tactic_expr ?(dflt=false) te tacfun gls =
+ abstract_operation (Tactic(te,dflt)) tacfun gls
-let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
+let abstract_tactic ?(dflt=false) te =
+ abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te))
-let abstract_extended_tactic s args =
- abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
+let abstract_extended_tactic ?(dflt=false) s args =
+ abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
let refiner = function
| Prim pr as r ->
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 0225e6443..b4b37fdf3 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -35,11 +35,12 @@ type transformation_tactic = proof_tree -> (goal list * validation)
(*s Hiding the implementation of tactics. *)
(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
- a single proof node *)
+ a single proof node. The boolean tells if the default tactic is used. *)
val abstract_operation : compound_rule -> tactic -> tactic
-val abstract_tactic : atomic_tactic_expr -> tactic -> tactic
-val abstract_tactic_expr : tactic_expr -> tactic -> tactic
-val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
+val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
+val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
+val abstract_extended_tactic :
+ ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic
val refiner : rule -> tactic
val frontier : transformation_tactic