Removing unused tactics in rewrite.

3 files changed, 0 insertions, 86 deletions

diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 31defcafb..db98c4250 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -265,19 +265,3 @@ TACTIC EXTEND setoid_transitivity
   [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
 | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
 END
-
-TACTIC EXTEND implify
-[ "implify" hyp(n) ] -> [ Proofview.V82.tactic (implify n) ]
-END
-
-TACTIC EXTEND fold_match
-[ "fold_match" constr(c) ] -> [ Proofview.V82.tactic (fold_match_tac c) ]
-END
-
-TACTIC EXTEND fold_matches
-| [ "fold_matches" constr(c) ] -> [ Proofview.V82.tactic (fold_matches_tac c) ]
-END
-
-TACTIC EXTEND myapply
-| [ "myapply" global(id) constr_list(l) ] -> [ Proofview.V82.tactic (myapply id l) ]
-END
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 22dc93d1a..a10b62162 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1818,65 +1818,3 @@ let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
 let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
 let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity
-
-
-let implify id gl =
-  let (_, b, ctype) = pf_get_hyp gl id in
-  let binders,concl = decompose_prod_assum ctype in
-  let ctype' =
-    match binders with
-    | (_, None, ty as hd) :: tl when noccurn 1 concl ->
-	let env = Environ.push_rel_context tl (pf_env gl) in
-	let sigma = project gl in
-	let tyhd = Typing.type_of env sigma ty
-	and tyconcl = Typing.type_of (Environ.push_rel hd env) sigma concl in
-	let app, unfold = arrow_morphism tyhd (subst1 mkProp tyconcl) ty (subst1 mkProp concl) in
-	it_mkProd_or_LetIn app tl
-    | _ -> ctype
-  in convert_hyp_no_check (id, b, ctype') gl
-
-let rec fold_matches eff env sigma c =
-  map_constr_with_full_binders Environ.push_rel
-    (fun env c ->
-      match kind_of_term c with
-      | Case _ ->
-          let cst, env, c',eff' = fold_match ~force:true env sigma c in
-          eff := Declareops.union_side_effects eff' !eff;
-          fold_matches eff env sigma c'
-      | _ -> fold_matches eff env sigma c)
-    env c
-
-let fold_matches_tac c gl =
-  let eff = ref Declareops.no_seff in
-  let c' = fold_matches eff (pf_env gl) (project gl) c in
-  tclTHEN (Tactics.emit_side_effects !eff)
-    (change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl) gl
-
-let myapply id l gl =
-  let gr = id in
-  let _, impls = List.hd (Impargs.implicits_of_global gr) in
-  let ty = Global.type_of_global gr in
-  let env = pf_env gl in
-  let evars = ref (project gl) in
-  let app =
-    let rec aux ty impls args args' =
-      match impls, kind_of_term ty with
-      | Some (_, _, (_, _)) :: impls, Prod (n, t, t') ->
-          let arg = Evarutil.e_new_evar evars env t in
-            aux (subst1 arg t') impls args (arg :: args')
-      | None :: impls, Prod (n, t, t') ->
-          (match args with
-            | [] ->
-                if dependent (mkRel 1) t' then
-                  let arg = Evarutil.e_new_evar evars env t in
-                    aux (subst1 arg t') impls args (arg :: args')
-                else
-                  let arg = Evarutil.mk_new_meta () in
-                    evars := meta_declare (destMeta arg) t !evars;
-                    aux (subst1 arg t') impls args (arg :: args')
-            | arg :: args ->
-                aux (subst1 arg t') impls args (arg :: args'))
-      | _, _ -> mkApp (constr_of_global gr, Array.of_list (List.rev args'))
-    in aux ty impls l []
-  in
-  tclTHEN (Refiner.tclEVARS !evars) (apply app) gl
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 63166c64a..e2d9a41d8 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -78,11 +78,3 @@ val setoid_symmetry_in : Id.t -> unit Proofview.tactic
 val setoid_reflexivity : unit Proofview.tactic
 
 val setoid_transitivity : constr option -> unit Proofview.tactic
-
-val implify : Id.t -> tactic
-
-val fold_match_tac : constr -> tactic
-
-val fold_matches_tac : constr -> tactic
-
-val myapply : Globnames.global_reference -> constr list -> tactic