diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-12 18:05:26 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-12 18:05:26 +0000 |
| commit | 6401e75b74e02078d0ac3e94ba9c336c0a6a834b (patch) | |
| tree | d9ae88eafdc8466231eda7d72c75ace4f2ee456c /proofs | |
| parent | 3725135942a9778cbc741602dc6ecba23dde46f8 (diff) | |
Ajout de _ dans les patterns d'intro
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1584 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_trees.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 1 |
4 files changed, 4 insertions, 0 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index b6867ef89..43bd3c749 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -348,6 +348,7 @@ let ast_of_cvt_bind f = function | (Com,c) -> ope ("BINDING", [ope ("COMMAND",[(f c)])]) let rec ast_of_cvt_intro_pattern = function + | WildPat -> ope ("WILDCAR",[]) | IdPat id -> nvar (string_of_id id) | DisjPat l -> ope ("DISJPATTERN", (List.map ast_of_cvt_intro_pattern l)) | ConjPat l -> ope ("CONJPATTERN", (List.map ast_of_cvt_intro_pattern l)) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index cf92c41e6..bf8deb53a 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -110,6 +110,7 @@ and tactic_arg = | Intropattern of intro_pattern and intro_pattern = + | WildPat | IdPat of identifier | DisjPat of intro_pattern list | ConjPat of intro_pattern list diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index a09504b36..de2c155f0 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -142,6 +142,7 @@ and tactic_arg = | Intropattern of intro_pattern and intro_pattern = + | WildPat | IdPat of identifier | DisjPat of intro_pattern list | ConjPat of intro_pattern list diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index b5f4d88f0..cf120ecdc 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -1120,6 +1120,7 @@ and redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) = function (* Interprets the patterns of Intro *) and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug) = function + | Node(_,"WILDCAR", []) -> WildPat | Node(_,"IDENTIFIER", [Nvar(loc,s)]) -> IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug) (Nvar (loc,s))))) |