diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-27 20:29:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-27 20:29:20 +0000 |
| commit | 9b3b1a9d73cac7ef55fc0744650eb0f668cb98a8 (patch) | |
| tree | df1da379e59f5b59df8b5d61d6c0151b69929751 /proofs/proof_type.ml | |
| parent | 93bd05ce0dc68892375a77df0d4ac7d73770c433 (diff) | |
Simplification de Proof_type.prim_rule
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2571 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 35 |
1 files changed, 14 insertions, 21 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index c84a147d9..afee5e2a9 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -31,27 +31,20 @@ type hyp_location = (* To distinguish body and type of local defs *) | InHyp of identifier | InHypType of identifier -type prim_rule_name = - | Intro - | Intro_after - | Intro_replacing - | Cut of bool - | FixRule - | Cofix - | Refine - | Convert_concl - | Convert_hyp - | Thin - | ThinBody - | Move of bool - | Rename - -type prim_rule = { - name : prim_rule_name; - hypspecs : identifier list; - newids : identifier list; - params : Coqast.t list; - terms : constr list } +type prim_rule = + | Intro of identifier + | Intro_replacing of identifier + | Cut of bool * identifier * types + | FixRule of identifier * int * (identifier * int * constr) list + | Cofix of identifier * (identifier * constr) list + | Refine of constr + | Convert_concl of types + | Convert_hyp of named_declaration + | Thin of identifier list + | ThinBody of identifier list + | Move of bool * identifier * identifier + | Rename of identifier * identifier + (* Signature useful to define the tactic type *) type 'a sigma = { |