diff options
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 b6867ef89f..43bd3c7497 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 cf92c41e6d..bf8deb53a5 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 a09504b366..de2c155f07 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 b5f4d88f02..cf120ecdc6 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))))) |