diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/proof_type.ml | 8 | ||||
-rw-r--r-- | proofs/proof_type.mli | 5 | ||||
-rw-r--r-- | proofs/refiner.ml | 11 | ||||
-rw-r--r-- | proofs/refiner.mli | 9 |
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 |