diff options
Diffstat (limited to 'proofs/tacinterp.ml')
| -rw-r--r-- | proofs/tacinterp.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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))))) |