Put the "cofix" tactic in the monad.

10 files changed, 61 insertions, 75 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 4893e4097..766f0714d 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -238,8 +238,8 @@ END
 (* Cofix *)
 
 TACTIC EXTEND cofix
-  [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ]
-| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ]
+  [ "cofix" ] -> [ Tactics.cofix None ]
+| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ]
 END
 
 (* Clear *)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 7acdff9ac..5aff262aa 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1729,7 +1729,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
-        let tac = Proofview.V82.tactic (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0) in
+        let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
diff --git a/printing/printer.ml b/printing/printer.ml
index 4c8e806f4..cb075c64f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -685,16 +685,6 @@ let pr_prim_rule = function
        (str"cut " ++ pr_constr t ++
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 
-  | Cofix (f,[],_) ->
-      (str"cofix " ++ pr_id f)
-
-  | Cofix (f,others,j) ->
-      if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
-      let rec print_mut = function
-	| (f,ar)::oth ->
-	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
-        | [] -> mt () in
-      (str"cofix " ++ pr_id f ++  str" with " ++ print_mut others)
   | Refine c ->
       str(if Termops.occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ec1b7ca86..36ae5554f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -543,47 +543,6 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
-    | Cofix (f,others,j) ->
-     	let rec check_is_coind env cl =
-	  let b = whd_betadeltaiota env sigma cl in
-          match kind_of_term b with
-            | Prod (na,c1,b) -> let open Context.Rel.Declaration in
-                                check_is_coind (push_rel (LocalAssum (na,c1)) env) b
-            | _ ->
-		try
-		  let _ = find_coinductive env sigma b in ()
-                with Not_found ->
-		  error "All methods must construct elements in coinductive types."
-	in
-	let firsts,lasts = List.chop j others in
-	let all = firsts@(f,cl)::lasts in
-     	List.iter (fun (_,c) -> check_is_coind env c) all;
-        let rec mk_sign sign = function
-          | (f,ar)::oth ->
-	      (try
-                (let _ = lookup_named_val f sign in
-                error "Name already used in the environment.")
-              with
-              |	Not_found ->
-                  mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth)
-	  | [] -> 
-              Evd.Monad.List.map (fun (_,c) sigma ->
-                let gl,ev,sigma =
-                  Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
-                (gl,ev),sigma)
-              all sigma
-     	in
-	let (gls_evs,sigma) =  mk_sign sign all in
-	let (gls,evs) = List.split gls_evs in
-	let (ids,types) = List.split all in
-	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
-	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
-	let typarray = Array.of_list types in
-	let bodies = Array.of_list evs in
-	let oterm = Term.mkCoFix (0,(funnames,typarray,bodies)) in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
-        (gls,sigma)
-
     | Refine c ->
 	check_meta_variables c;
 	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index ea3b5242d..ef0d52b62 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -19,7 +19,6 @@ open Misctypes
 
 type prim_rule =
   | Cut of bool * bool * Id.t * types
-  | Cofix of Id.t * (Id.t * constr) list * int
   | Refine of constr
   | Move of Id.t * Id.t move_location
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8eb8b2cec..8c0b4ba98 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -124,9 +124,6 @@ let refine_no_check c gl =
 let move_hyp_no_check id1 id2 gl =
   refiner (Move (id1,id2)) gl
 
-let mutual_cofix f others j gl =
-  with_check (refiner (Cofix (f,others,j))) gl
-
 (* Versions with consistency checks *)
 
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e2d8bfc6e..182433cb3 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -86,7 +86,6 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 val refiner                   : rule -> tactic
 val internal_cut_no_check     : bool -> Id.t -> types -> tactic
 val refine_no_check           : constr -> tactic
-val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
 
 (** {6 The most primitive tactics with consistency and type checking } *)
 
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 8db8de992..ce5ef0169 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -385,7 +385,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
 let rec_tac_initializer finite guard thms snl =
   if finite then
     match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
-    | (id,_)::l -> Proofview.V82.tactic (Tactics.mutual_cofix id l 0)
+    | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
     (* nl is dummy: it will be recomputed at Qed-time *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dc018a670..c3d6a65eb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -472,6 +472,14 @@ let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id))
 (*          Fixpoints and CoFixpoints                         *)
 (**************************************************************)
 
+let rec mk_holes : type r s. _ -> r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma =
+fun env sigma p -> function
+| [] -> Sigma ([], sigma, p)
+| arg :: rem ->
+  let Sigma (arg, sigma, q) = Evarutil.new_evar env sigma arg in
+  let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in
+  Sigma (arg :: rem, sigma, r)
+
 let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) with
 | Prod (na, c1, b) ->
   if Int.equal k 1 then
@@ -506,15 +514,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
   Refine.refine { run = begin fun sigma ->
-    let rec map : type r s. r Sigma.t -> (s, r) Sigma.le -> _ -> (_, s) Sigma.sigma =
-    fun sigma p -> function
-    | [] -> Sigma ([], sigma, p)
-    | (_, _, arg) :: rem ->
-      let Sigma (arg, sigma, q) = Evarutil.new_evar nenv sigma arg in
-      let Sigma (rem, sigma, r) = map sigma (p +> q) rem in
-      Sigma (arg :: rem, sigma, r)
-    in
-    let Sigma (evs, sigma, p) = map sigma Sigma.refl all in
+    let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl (List.map pi3 all) in
     let ids = List.map pi1 all in
     let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
     let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
@@ -536,14 +536,56 @@ let fix ido n = match ido with
   | Some id ->
     mutual_fix id n [] 0
 
+let rec check_is_mutcoind env sigma cl =
+  let b = whd_betadeltaiota env sigma cl in
+  match kind_of_term b with
+  | Prod (na, c1, b) ->
+    let open Context.Rel.Declaration in
+    check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b
+  | _ ->
+    try
+      let _ = find_coinductive env sigma b in ()
+    with Not_found ->
+      error "All methods must construct elements in coinductive types."
+
 (* Refine as a cofixpoint *)
-let mutual_cofix = Tacmach.mutual_cofix
+let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project gl in
+  let concl = Proofview.Goal.concl gl in
+  let firsts,lasts = List.chop j others in
+  let all = firsts @ (f, concl) :: lasts in
+  List.iter (fun (_, c) -> check_is_mutcoind env sigma c) all;
+  let rec mk_sign sign = function
+  | [] -> sign
+  | (f, ar) :: oth ->
+    let open Context.Named.Declaration in
+    if mem_named_context f (named_context_of_val sign) then
+      error "Name already used in the environment.";
+    mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
+  in
+  let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
+  Refine.refine { run = begin fun sigma ->
+    let (ids, types) = List.split all in
+    let Sigma (evs, sigma, p) = mk_holes nenv sigma Sigma.refl types in
+    let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
+    let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+    let typarray = Array.of_list types in
+    let bodies = Array.of_list evs in
+    let oterm = Term.mkCoFix (0, (funnames, typarray, bodies)) in
+    Sigma (oterm, sigma, p)
+  end }
+end }
 
-let cofix ido gl = match ido with
+let cofix ido = match ido with
   | None ->
-      mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] 0 gl
+    Proofview.Goal.enter { enter = begin fun gl ->
+      let name = Pfedit.get_current_proof_name () in
+      let id = new_fresh_id [] name gl in
+      mutual_cofix id [] 0
+    end }
   | Some id ->
-      mutual_cofix id [] 0 gl
+      mutual_cofix id [] 0
 
 (**************************************************************)
 (*          Reduction and conversion tactics                  *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 12364d211..f730dd6c4 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -38,8 +38,8 @@ val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
 val fix             : Id.t option -> int -> unit Proofview.tactic
-val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
-val cofix           : Id.t option -> tactic
+val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic
+val cofix           : Id.t option -> unit Proofview.tactic
 
 val convert         : constr -> constr -> unit Proofview.tactic
 val convert_leq     : constr -> constr -> unit Proofview.tactic