Adapt pieces of code needing -rectypes

 * in Matching and Tacinterp : ad-hoc types for encoding matching
   result and "next" continuation

 * in Class_tactics, occurrences of types such as
    "type t = (foo * (unit->t) option"
   have been specialized to something like
     type t = TNone | TSome of foo * (unit -> t)

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

2 files changed, 16 insertions, 10 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 217398a6da..4beaf5282c 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -252,13 +252,20 @@ let matches c p = snd (matches_core_closed None true c p)
 
 let special_meta = (-1)
 
+type 'a matching_result =
+    { m_sub : bound_ident_map * patvar_map;
+      m_ctx : 'a;
+      m_nxt : unit -> 'a matching_result }
+
+let mkresult s c n = { m_sub=s; m_ctx=c; m_nxt=n }
+
 (* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ partial_app closed pat c mk_ctx next =
   try
     let sigma = matches_core_closed None partial_app pat c in
     if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
     then next ()
-    else sigma, mk_ctx (mkMeta special_meta), next
+    else mkresult sigma (mk_ctx (mkMeta special_meta)) next
   with
     PatternMatchingFailure -> next ()
 
@@ -330,9 +337,6 @@ let sub_match ?(partial_app=false) ?(closed=true) pat c =
     try_sub_match_rec [] lc in
   aux c (fun x -> x) (fun () -> raise PatternMatchingFailure)
 
-type subterm_matching_result =
-    (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
-
 let match_subterm pat c = sub_match pat c
 
 let match_appsubterm pat c = sub_match ~partial_app:true pat c
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 9b412692ce..273c4d0612 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -50,27 +50,29 @@ val is_matching : 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 with [special_meta]) + a continuation that
+   (whose hole is denoted here with [special_meta]) + a continuation that
    either returns the next matching subterm or raise PatternMatchingFailure *)
-type subterm_matching_result =
-    (bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
+type 'a matching_result =
+    { m_sub : bound_ident_map * patvar_map;
+      m_ctx : 'a;
+      m_nxt : unit -> 'a matching_result }
 
 (** [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.
    It raises PatternMatchingFailure if no subterm matches the pattern *)
-val match_subterm : constr_pattern -> constr -> subterm_matching_result
+val match_subterm : constr_pattern -> constr -> constr matching_result
 
 (** [match_appsubterm pat c] returns the substitution and the context
    corresponding to the first **closed** subterm of [c] matching [pat],
    considering application contexts as well. It also returns a
    continuation that looks for the next matching subterm.
    It raises PatternMatchingFailure if no subterm matches the pattern *)
-val match_appsubterm : constr_pattern -> constr -> subterm_matching_result
+val match_appsubterm : constr_pattern -> constr -> constr matching_result
 
 (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
 val match_subterm_gen : bool (** true = with app context *) ->
-   constr_pattern -> constr -> subterm_matching_result
+   constr_pattern -> constr -> constr matching_result
 
 (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
    against [pat] taking partial subterms into consideration *)