Putting all the tactics exported by the Tactics module in the new monad API.

4 files changed, 3 insertions, 118 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 09f308abef..fd8a70c650 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -77,10 +77,10 @@ let with_check = Flags.with_option check
 
 (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
    returns [tail::(f head (id,_,_) (rev tail))] *)
-let apply_to_hyp sign id f =
+let apply_to_hyp check sign id f =
   try apply_to_hyp sign id f
   with Hyp_not_found ->
-    if !check then error_no_such_hypothesis id
+    if check then error_no_such_hypothesis id
     else sign
 
 let check_typability env sigma c =
@@ -493,7 +493,7 @@ let convert_hyp check sign sigma d =
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
-    apply_to_hyp sign id
+    apply_to_hyp check sign id
       (fun _ d' _ ->
         let _,c,ct = to_tuple d' in
         let env = Global.env_of_context sign in
@@ -543,92 +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
-          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
@@ -636,16 +550,6 @@ let prim_refiner r sigma goal =
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
 	  (sgl, sigma)
 
-    (* And now the structural rules *)
-    | Thin ids ->
-        let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
-	let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in
-	let (gl,ev,sigma) =
-	  Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
-	in
-	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-	  ([gl], sigma)
-
     | Move (hfrom, hto) ->
   	let (left,right,declfrom,toleft) =
 	  split_sign hfrom hto (named_context_of_val sign) in
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index b4c9dae2a3..ef0d52b62d 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -19,10 +19,7 @@ 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
-  | Thin of Id.t list
   | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 33cef7486b..8c0b4ba98a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -121,25 +121,14 @@ let internal_cut_rev_no_check replace id t gl =
 let refine_no_check c gl =
   refiner (Refine c) gl
 
-(* This does not check dependencies *)
-let thin_no_check ids gl =
-  if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) 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
-
 (* Versions with consistency checks *)
 
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
-let thin c             = with_check (thin_no_check c)
 let move_hyp id id'  = with_check (move_hyp_no_check id id')
 
 (* Pretty-printers *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f786b5f218..182433cb3a 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -86,17 +86,12 @@ 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 thin_no_check             : Id.t list -> 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 } *)
 
 val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
-val thin             : Id.t list -> tactic
 val move_hyp         : Id.t -> Id.t move_location -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)