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

4 files changed, 76 insertions, 44 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 217398a6d..4beaf5282 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 9b412692c..273c4d061 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 *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index d411a28c4..1fc013496 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -217,6 +217,16 @@ type auto_result = autogoal list sigma
 
 type atac = auto_result tac
 
+(* Some utility types to avoid the need of -rectypes *)
+
+type 'a optionk =
+  | Nonek
+  | Somek of 'a * 'a optionk fk
+
+type ('a,'b) optionk2 =
+  | Nonek2
+  | Somek2 of 'a * 'b * ('a,'b) optionk2 fk
+
 let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
   let cty = Evarutil.nf_evar sigma cty in
   let rec iscl env ty = 
@@ -408,21 +418,23 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
 		        (Goal.V82.env s gl) s' info.is_evar (Goal.V82.concl s gl)
 		    else true
 		  in
-		  let fk'' = 
+		  let fk'' =
 		    if not needs_backtrack then
-		      (if !typeclasses_debug then msg_debug (str"no backtrack on " ++ pr_ev s gl ++ 
-							 str " after " ++ Lazy.force info.auto_last_tac); fk) 
-		    else fk' 
+		      (if !typeclasses_debug then
+			  msg_debug (str"no backtrack on " ++ pr_ev s gl ++
+				     str " after " ++ Lazy.force info.auto_last_tac);
+		       fk)
+		    else fk'
 		  in aux s' (gls'::acc) fk'' gls)
 	       fk {it = (gl,info); sigma = s})
-    | [] -> Some (List.rev acc, s, fk)
+    | [] -> Somek2 (List.rev acc, s, fk)
   in fun {it = gls; sigma = s} fk ->
     let rec aux' = function
-      | None -> fk ()
-      | Some (res, s', fk') ->
+      | Nonek2 -> fk ()
+      | Somek2 (res, s', fk') ->
 	  let goals' = List.concat res in
 	    sk {it = goals'; sigma = s'} (fun () -> aux' (fk' ()))
-    in aux' (aux s [] (fun () -> None) gls)
+    in aux' (aux s [] (fun () -> Nonek2) gls)
 
 let then_tac (first : atac) (second : atac) : atac =
   { skft = fun sk fk -> first.skft (then_list second sk) fk }
@@ -430,12 +442,12 @@ let then_tac (first : atac) (second : atac) : atac =
 let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
   t.skft (fun x _ -> Some x) (fun _ -> None) gl
 
-type run_list_res = (auto_result * run_list_res fk) option
+type run_list_res = auto_result optionk
 
 let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
-  (then_list t (fun x fk -> Some (x, fk)))
+  (then_list t (fun x fk -> Somek (x, fk)))
     gl
-    (fun _ -> None)
+    (fun _ -> Nonek)
 
 let fail_tac : atac = 
   { skft = fun sk fk _ -> fk () }
@@ -465,8 +477,8 @@ let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs ev
 
 let get_result r = 
   match r with
-  | None -> None
-  | Some (gls, fk) -> Some (gls.sigma,fk)
+  | Nonek -> None
+  | Somek (gls, fk) -> Some (gls.sigma,fk)
 	
 let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm hints tac =
   match evars_to_goals p evm with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2ed054ea1..215dee837 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1672,6 +1672,11 @@ let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
 
 let adjust (l,lc) = (l,List.map (fun (id,c) -> (id,([],c))) lc)
 
+type 'a extended_matching_result =
+    { e_ctx : 'a;
+      e_sub : bound_ident_map * extended_patvar_map;
+      e_nxt : unit -> 'a extended_matching_result }
+
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
 let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
   let get_id_couple id = function
@@ -1683,27 +1688,34 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
         let lmeta = extended_matches t hyp in
         (try
             let lmeta = verify_metas_coherence gl lmatch lmeta in
-            ([],lmeta,(fun () -> raise PatternMatchingFailure))
+            { e_ctx = [];
+	      e_sub = lmeta;
+	      e_nxt = fun () -> raise PatternMatchingFailure }
           with
-            | Not_coherent_metas -> raise PatternMatchingFailure);
+            | Not_coherent_metas -> raise PatternMatchingFailure)
     | Subterm (b,ic,t) ->
         let rec match_next_pattern find_next () =
-          let (lmeta,ctxt,find_next') = find_next () in
+          let s = find_next () in
           try
-            let lmeta = verify_metas_coherence gl lmatch (adjust lmeta) in
-            (give_context ctxt ic,lmeta,match_next_pattern find_next')
+            let lmeta = verify_metas_coherence gl lmatch (adjust s.m_sub) in
+            { e_ctx = give_context s.m_ctx ic;
+	      e_sub = lmeta;
+	      e_nxt = match_next_pattern s.m_nxt }
           with
-            | Not_coherent_metas -> match_next_pattern find_next' () in
-        match_next_pattern (fun () -> match_subterm_gen b t hyp) () in
+            | Not_coherent_metas -> match_next_pattern s.m_nxt ()
+	in
+        match_next_pattern (fun () -> match_subterm_gen b t hyp) ()
+  in
   let rec apply_one_mhyp_context_rec = function
     | (id,b,hyp as hd)::tl ->
 	(match patv with
 	| None ->
             let rec match_next_pattern find_next () =
               try
-                let (ids, lmeta, find_next') = find_next () in
-		(get_id_couple id hypname@ids, lmeta, hd,
-                 match_next_pattern find_next')
+                let s = find_next () in
+		{ e_ctx = (get_id_couple id hypname @ s.e_ctx), hd;
+		  e_sub = s.e_sub;
+                  e_nxt = match_next_pattern s.e_nxt }
               with
                 | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in
             match_next_pattern (fun () ->
@@ -1714,19 +1726,20 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
 	    | Some body ->
                 let rec match_next_pattern_in_body next_in_body () =
                   try
-                    let (ids,lmeta,next_in_body') = next_in_body() in
+                    let s1 = next_in_body() in
                     let rec match_next_pattern_in_typ next_in_typ () =
                       try
-                        let (ids',lmeta',next_in_typ') = next_in_typ() in
-		        (get_id_couple id hypname@ids@ids', lmeta', hd,
-                         match_next_pattern_in_typ next_in_typ')
+			let s2 = next_in_typ() in
+		        { e_ctx = (get_id_couple id hypname@s1.e_ctx@s2.e_ctx), hd;
+			  e_sub = s2.e_sub;
+			  e_nxt = match_next_pattern_in_typ s2.e_nxt }
                       with
                         | PatternMatchingFailure ->
-                            match_next_pattern_in_body next_in_body' () in
+                            match_next_pattern_in_body s1.e_nxt () in
                     match_next_pattern_in_typ
                       (fun () ->
 			let hyp = refresh_universes_strict hyp in
-			match_pat lmeta hyp pat) ()
+			match_pat s1.e_sub hyp pat) ()
                   with PatternMatchingFailure -> apply_one_mhyp_context_rec tl
                 in
                 match_next_pattern_in_body
@@ -1993,7 +2006,7 @@ and interp_match_goal ist goal lz lr lmr =
   let env = pf_env goal in
   let apply_goal_sub app ist (id,c) csr mt mhyps hyps =
     let rec match_next_pattern find_next () =
-      let (lgoal,ctxt,find_next') = find_next () in
+      let { m_sub=lgoal; m_ctx=ctxt; m_nxt=find_next' } = find_next () in
       let lctxt = give_context ctxt id in
       try apply_hyps_context ist env lz goal mt lctxt (adjust lgoal) mhyps hyps
       with e when is_match_catchable e -> match_next_pattern find_next' () in
@@ -2049,14 +2062,15 @@ and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
 	  | Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp
 	in
         let rec match_next_pattern find_next =
-          let (lids,lm,hyp_match,find_next') = find_next () in
+          let s = find_next () in
+	  let lids,hyp_match = s.e_ctx in
           db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
 	  try
             let id_match = pi1 hyp_match in
             let nextlhyps = List.remove_assoc_in_triple id_match lhyps_rest in
-            apply_hyps_context_rec (lfun@lids) lm nextlhyps tl
+            apply_hyps_context_rec (lfun@lids) s.e_sub nextlhyps tl
           with e when is_match_catchable e ->
-	    match_next_pattern find_next' in
+	    match_next_pattern s.e_nxt in
         let init_match_pattern () =
           apply_one_mhyp_context ist env goal lmatch hyp_pat lhyps_rest in
         match_next_pattern init_match_pattern
@@ -2186,7 +2200,7 @@ and interp_genarg_var_list1 ist gl x =
 and interp_match ist g lz constr lmr =
   let apply_match_subterm app ist (id,c) csr mt =
     let rec match_next_pattern find_next () =
-      let (lmatch,ctxt,find_next') = find_next () in
+      let { m_sub=lmatch; m_ctx=ctxt; m_nxt=find_next' } = find_next () in
       let lctxt = give_context ctxt id in
       let lfun = extend_values_with_bindings (adjust lmatch) (lctxt@ist.lfun) in
       try eval_with_fail {ist with lfun=lfun} lz g mt