diff options
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 832377e31..6688d6e62 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -22,10 +22,6 @@ open Misctypes (** This module defines the structure of proof tree and the tactic type. So, it is used by [Proof_tree] and [Refiner] *) -type goal = Goal.goal - -type tactic = goal sigma -> goal list sigma - type prim_rule = | Intro of identifier | Cut of bool * bool * identifier * types @@ -41,6 +37,10 @@ type prim_rule = | Rename of identifier * identifier | Change_evars +(** Nowadays, the only rules we'll consider are the primitive rules *) + +type rule = prim_rule + (** The type [goal sigma] is the type of subgoal. It has the following form {v it = \{ evar_concl = [the conclusion of the subgoal] evar_hyps = [the hypotheses of the subgoal] @@ -66,13 +66,12 @@ type prim_rule = in the type of evar] \} \} \} v} *) -type rule = Prim of prim_rule +type goal = Goal.goal -type compound_rule= - (** the boolean of Tactic tells if the default tactic is used *) - | Tactic of tactic_expr * bool +type tactic = goal sigma -> goal list sigma -and tactic_expr = + +type tactic_expr = (constr, constr_pattern, evaluable_global_reference, @@ -105,6 +104,8 @@ and tactic_arg = tlevel) Tacexpr.gen_tactic_arg +(** Ltac traces *) + type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant |