Put the "fix" tactic in the monad.

13 files changed, 72 insertions, 80 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 4e2dfafb52..98b77ab357 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -231,8 +231,8 @@ END
 (* Fix *)
 
 TACTIC EXTEND fix
-  [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ]
-| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ]
+  [ "fix" natural(n) ] -> [ Tactics.fix None n ]
+| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ]
 END
 
 (* Cofix *)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index d650cb5c6f..5e0153fcee 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1714,7 +1714,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_fix (interp_ident ist env sigma id) n l_interp 0) in
+        let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 4f22703130..a6b3381648 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1385,7 +1385,7 @@ let end_tac et2 gls =
 		      let c_id =
 			pf_get_new_id (Id.of_string "_main_arg") gls0 in
 			tclTHENLIST
-			  [fix (Some fix_id) (succ nargs);
+			  [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs));
 			   tclDO nargs (Proofview.V82.of_tactic introf);
 			   Proofview.V82.of_tactic (intro_mustbe_force c_id);
 			   execute_cases (Name fix_id) pi
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index fdb112ba01..0b7a1e6468 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1227,10 +1227,10 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	      if this_fix_info.idx + 1 = 0
 	      then tclIDTAC (* Someone  tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
 	      else
-		observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (fix (Some this_fix_info.name) (this_fix_info.idx +1))
+		observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1)))
 	    else
-	      Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
-		other_fix_infos 0
+	      Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
+		other_fix_infos 0)
 	| _ -> anomaly (Pp.str "Not a valid information")
     in
     let first_tac : tactic = (* every operations until fix creations *)
@@ -1642,7 +1642,7 @@ let prove_principle_for_gen
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
 (* 			   str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
-      (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1));
+      (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ac81366bb5..c1c3801b45 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1119,7 +1119,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 			tclTHEN (Tactics.generalize [mkVar id]) (Proofview.V82.of_tactic (clear [id])))
 		     ))
 	       ;
-		observe_tac (str "fix") (fix (Some hrec) (nargs+1));
+		observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
 		h_intros args_id;
 		Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
 		observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
diff --git a/printing/printer.ml b/printing/printer.ml
index 401f5f99e9..4c8e806f43 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -685,18 +685,6 @@ let pr_prim_rule = function
        (str"cut " ++ pr_constr t ++
         str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
 
-  | FixRule (f,n,[],_) ->
-      (str"fix " ++ pr_id f ++ str"/" ++ int n)
-
-  | FixRule (f,n,others,j) ->
-      if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\"");
-      let rec print_mut = function
-	| (f,n,ar)::oth ->
-           pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
-        | [] -> mt () in
-      (str"fix " ++ pr_id f ++ str"/" ++ int n ++
-         str" with " ++ print_mut others)
-
   | Cofix (f,[],_) ->
       (str"cofix " ++ pr_id f)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index df5a12473b..ec1b7ca869 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -543,51 +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)
 
-    | FixRule (f,n,rest,j) ->
-     	let rec check_ind env k cl =
-          match kind_of_term (strip_outer_cast cl) with
-            | Prod (na,c1,b) ->
-            	if Int.equal k 1 then
-		  try
-		    fst (find_inductive env sigma c1)
-		  with Not_found ->
-		    error "Cannot do a fixpoint on a non inductive type."
-            	else
-                  let open Context.Rel.Declaration in
-		  check_ind (push_rel (LocalAssum (na,c1)) env) (k-1) b
-            | _ -> error "Not enough products."
-	in
-	let ((sp,_),u) = check_ind env n cl in
-	let firsts,lasts = List.chop j rest in
-	let all = firsts@(f,n,cl)::lasts in
-     	let rec mk_sign sign = function
-	  | (f,n,ar)::oth ->
-	      let ((sp',_),u')  = check_ind env n ar in
-	      if not (eq_mind sp sp') then
-		error "Fixpoints should be on the same mutual inductive declaration.";
-	      if !check && mem_named_context f (named_context_of_val sign) then
-		errorlabstrm "Logic.prim_refiner"
-		  (str "Name " ++ pr_id f ++ str " already used in the environment");
-	      mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth
-	  | [] ->
-	      Evd.Monad.List.map (fun (_,_,c) sigma ->
-                let gl,ev,sig' =
-                  Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in
-                (gl,ev),sig')
-              all sigma
-	in
-	let (gls_evs,sigma) =  mk_sign sign all in
-	let (gls,evs) = List.split gls_evs 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
-	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
-	let typarray = Array.of_list (List.map pi3 all) in
-	let bodies = Array.of_list evs in
-	let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
-	(gls,sigma)
-
     | Cofix (f,others,j) ->
      	let rec check_is_coind env cl =
 	  let b = whd_betadeltaiota env sigma cl in
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 48ad50c7a0..ea3b5242da 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
-  | FixRule of Id.t * int * (Id.t * int * constr) list * int
   | 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 67daccb81d..8eb8b2cec6 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_fix f n others j gl =
-  with_check (refiner (FixRule (f,n,others,j))) gl
-
 let mutual_cofix f others j gl =
   with_check (refiner (Cofix (f,others,j))) gl
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index fef205f823..e2d8bfc6ef 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -86,8 +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_fix      :
-  Id.t -> int -> (Id.t * int * constr) list -> int -> 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 80b3fef196..8db8de9927 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 -> Tactics.mutual_cofix id l 0
+    | (id,_)::l -> Proofview.V82.tactic (Tactics.mutual_cofix id l 0)
     | _ -> assert false
   else
     (* nl is dummy: it will be recomputed at Qed-time *)
@@ -403,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
     | Anonymous -> Tactics.intro) (List.rev ids) in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
-      let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+      let rec_tac = rec_tac_initializer finite guard thms snl in
       Some (match init_tac with
         | None -> 
             if Flags.is_auto_intros () then 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a47ee96a0a..01af30049b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -472,14 +472,69 @@ let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id))
 (*          Fixpoints and CoFixpoints                         *)
 (**************************************************************)
 
+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
+    try
+      let ((sp, _), u), _ = find_inductive env sigma c1 in
+      (sp, u)
+    with Not_found -> error "Cannot do a fixpoint on a non inductive type."
+  else
+    let open Context.Rel.Declaration in
+    check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b
+| _ -> error "Not enough products."
+
 (* Refine as a fixpoint *)
-let mutual_fix = Tacmach.mutual_fix
+let mutual_fix f n rest 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 (sp, u) = check_mutind env sigma n concl in
+  let firsts, lasts = List.chop j rest in
+  let all = firsts @ (f, n, concl) :: lasts in
+  let rec mk_sign sign = function
+  | [] -> sign
+  | (f, n, ar) :: oth ->
+    let open Context.Named.Declaration in
+    let (sp', u')  = check_mutind env sigma n ar in
+    if not (eq_mind sp sp') then
+      error "Fixpoints should be on the same mutual inductive declaration.";
+    if mem_named_context f (named_context_of_val sign) then
+      errorlabstrm "Logic.prim_refiner"
+        (str "Name " ++ pr_id f ++ str " 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 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 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
+    let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
+    let typarray = Array.of_list (List.map pi3 all) in
+    let bodies = Array.of_list evs in
+    let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in
+    Sigma (oterm, sigma, p)
+  end }
+end }
 
-let fix ido n gl = match ido with
+let fix ido n = match ido with
   | None ->
-      mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] 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_fix id n [] 0
+    end }
   | Some id ->
-      mutual_fix id n [] 0 gl
+    mutual_fix id n [] 0
 
 (* Refine as a cofixpoint *)
 let mutual_cofix = Tacmach.mutual_cofix
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f6c001941c..47ff197a05 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -36,8 +36,8 @@ val convert_hyp     : ?check:bool -> Context.Named.Declaration.t -> unit Proofvi
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
 val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
 val mutual_fix      :
-  Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
-val fix             : Id.t option -> int -> tactic
+  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