diff options
Diffstat (limited to 'tactics/pattern.mli')
| -rw-r--r-- | tactics/pattern.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tactics/pattern.mli b/tactics/pattern.mli index fc9d07ef7f..afe1ec848e 100644 --- a/tactics/pattern.mli +++ b/tactics/pattern.mli @@ -47,9 +47,7 @@ val put_pat : module_mark -> string -> marked_term val get_pat : marked_term -> constr val pattern_stock : constr Stock.stock -(*i** -val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr -**i*) +val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr (*s Second part : Given a term with second-order variables in it, represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to |