From 326c5769968d85bc0dc294c768585129d56e57d4 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Thu, 14 Nov 2013 15:21:38 +0000
Subject: Update comments in matching.mli.

The comments were inaccurate after r16533.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17088 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/matching.mli | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index c9bf60ad28..b82f115251 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -58,19 +58,17 @@ val is_matching_head : constr_pattern -> constr -> bool
 val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
 
 (** The type of subterm matching results: a substitution + a context
-   (whose hole is denoted here with [special_meta]) + a continuation that
-   either returns the next matching subterm or raise PatternMatchingFailure *)
+   (whose hole is denoted here with [special_meta]) *)
 type matching_result =
     { m_sub : bound_ident_map * patvar_map;
       m_ctx : constr }
 
 (** [match_subterm n pat c] returns the substitution and the context
-   corresponding to the first **closed** subterm of [c] matching [pat], and
-   a continuation that looks for the next matching subterm. *)
+   corresponding to each **closed** subterm of [c] matching [pat]. *)
 val match_subterm : constr_pattern -> constr -> matching_result IStream.t
 
 (** [match_appsubterm pat c] returns the substitution and the context
-   corresponding to the first **closed** subterm of [c] matching [pat],
+   corresponding to each **closed** subterm of [c] matching [pat],
    considering application contexts as well. *)
 val match_appsubterm : constr_pattern -> constr -> matching_result IStream.t
 
-- 
cgit v1.2.3