diff options
| author | filliatr | 1999-12-05 18:46:38 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-05 18:46:38 +0000 |
| commit | c70bdc0f7ddfca7055d1af4d81086485518056af (patch) | |
| tree | 081e2cb705e150d9b49b6cda91bb6e3ad58d67fa /tactics/pattern.mli | |
| parent | e22c71e0edeccc537bb8e584812ad0646ec0dd84 (diff) | |
premier debugage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |