Pattern matching de sous-termes + exceptions dans le lexer

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@578 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 1 deletions

diff --git a/parsing/pattern.mli b/parsing/pattern.mli
index b725d9044..803e4fffe 100644
--- a/parsing/pattern.mli
+++ b/parsing/pattern.mli
@@ -69,9 +69,15 @@ val is_matching      :
 val matches_conv :
   env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
 
+(* To skip to the next occurrence *)
+exception NextOccurrence of int
+
+(* Tries to match a subterm of [c] with [pat] *)
+val sub_match :
+  int -> constr_pattern -> constr -> ((int * constr) list * constr)
+
 (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
    up to conversion for constants in patterns *)
 
 val is_matching_conv :
   env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool
-