diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-08-17 16:15:07 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-08-17 16:15:07 +0000 |
| commit | c85ee5577d9ee20a9a91c338ece3c1c0685874b7 (patch) | |
| tree | b869ecea99abb4ba7f15251200a96fc931292911 /proofs/proof_type.ml | |
| parent | 0406263287e722c7784bc66225da4ef13118f2da (diff) | |
Pattern matching de sous-termes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@579 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 462b038a1..d90d3a93a 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -83,21 +83,22 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_arg = - Command of Coqast.t - | Constr of constr - | Identifier of identifier - | Integer of int - | Clause of identifier list - | Bindings of Coqast.t substitution - | Cbindings of constr substitution - | Quoted_string of string - | Tacexp of Coqast.t - | Tac of tactic - | Redexp of Tacred.red_expr - | Fixexp of identifier * int * Coqast.t - | Cofixexp of identifier * Coqast.t - | Letpatterns of (int list option * (identifier * int list) list) - | Intropattern of intro_pattern + | Command of Coqast.t + | Constr of constr + | Constr_context of constr + | Identifier of identifier + | Integer of int + | Clause of identifier list + | Bindings of Coqast.t substitution + | Cbindings of constr substitution + | Quoted_string of string + | Tacexp of Coqast.t + | Tac of tactic + | Redexp of Tacred.red_expr + | Fixexp of identifier * int * Coqast.t + | Cofixexp of identifier * Coqast.t + | Letpatterns of (int list option * (identifier * int list) list) + | Intropattern of intro_pattern and intro_pattern = | IdPat of identifier |