Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans sub_match qui est renommé par ailleurs en match_subterm

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

2 files changed, 8 insertions, 5 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 645684a86..237ec0db8 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -242,6 +242,10 @@ and try_sub_match nocc pat lc =
       | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in
   try_sub_match_rec nocc pat [] lc
 
+let match_subterm nocc pat c =
+  try sub_match nocc pat c
+  with NextOccurrence _ -> raise PatternMatchingFailure
+
 let is_matching pat n =
   try let _ = matches pat n in true
   with PatternMatchingFailure -> false
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 886d87ae0..2b0b8f240 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -39,11 +39,10 @@ val is_matching : constr_pattern -> constr -> bool
 
 val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
 
-(* To skip to the next occurrence *)
-exception NextOccurrence of int
-
-(* Tries to match a _closed_ subterm of [c] with [pat] *)
-val sub_match : int -> constr_pattern -> constr -> patvar_map * constr
+(* [match_subterm n pat c] returns the substitution and the context
+   corresponding to the [n+1]th _closed_ subterm of [c] matching [pat];
+   It raises PatternMatchingFailure if no such matching exists *)
+val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr
 
 (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
    up to conversion for constants in patterns *)