diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:29 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 10:08:29 +0000 |
| commit | a0057a6657f5615c3d3448fae10b26a968d30fe1 (patch) | |
| tree | 0617fe67223c46d7fd1f17c83068ee6ca98d74ab /proofs/proof_type.ml | |
| parent | 4a8188a2b460ab014379c508abac933690b48555 (diff) | |
Proof_type: rule now degenerates to prim_rule
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index d806d80b8..b84b6db48 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -21,6 +21,8 @@ open Misctypes (* This module defines the structure of proof tree and the tactic type. So, it is used by Proof_tree and Refiner *) +(** Types of goals, tactics, rules ... *) + type goal = Goal.goal type tactic = goal sigma -> goal list sigma @@ -40,12 +42,11 @@ type prim_rule = | Rename of identifier * identifier | Change_evars -type rule = Prim of prim_rule +(** Nowadays, the only rules we'll consider are the primitive rules *) -type compound_rule= - | Tactic of tactic_expr * bool +type rule = prim_rule -and tactic_expr = +type tactic_expr = (constr, constr_pattern, evaluable_global_reference, @@ -78,6 +79,8 @@ and tactic_arg = tlevel) Tacexpr.gen_tactic_arg +(** Ltac traces *) + type ltac_call_kind = | LtacNotationCall of string | LtacNameCall of ltac_constant |