rename-everything

2 files changed, 0 insertions, 573 deletions

diff --git a/src/Tactics/Algebra_syntax/Nsatz.v b/src/Tactics/Algebra_syntax/Nsatz.v
deleted file mode 100644
index e219bc579..000000000
--- a/src/Tactics/Algebra_syntax/Nsatz.v
+++ /dev/null
@@ -1,159 +0,0 @@
-(*** Tactics for manipulating polynomial equations *)
-Require Coq.nsatz.Nsatz.
-Require Import Coq.Lists.List.
-
-Generalizable All Variables.
-Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)}
-  : forall x y, eq (sub x y) zero <-> eq x y.
-Proof.
-  split;intros Hx.
-  { eapply Nsatz.psos_r1b. eapply Hx. }
-  { eapply Nsatz.psos_r1. eapply Hx. }
-Qed.
-
-Ltac get_goal := lazymatch goal with |- ?g => g end.
-
-Ltac nsatz_equation_implications_to_list eq zero g :=
-  lazymatch g with
-  | eq ?p zero => constr:(p::nil)
-  | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l)
-  end.
-
-Ltac nsatz_reify_equations eq zero :=
-  let g := get_goal in
-  let lb := nsatz_equation_implications_to_list eq zero g in
-  lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with
-    (?variables, ?le) =>
-    lazymatch (eval compute in (List.rev le)) with
-    | ?reified_goal::?reified_givens => constr:((variables, reified_givens, reified_goal))
-    end
-  end.
-
-Ltac nsatz_get_free_variables reified_package :=
-  lazymatch reified_package with (?fv, _, _) => fv end.
-
-Ltac nsatz_get_reified_givens reified_package :=
-  lazymatch reified_package with (_, ?givens, _) => givens end.
-
-Ltac nsatz_get_reified_goal reified_package :=
-  lazymatch reified_package with (_, _, ?goal) => goal end.
-
-Require Import Coq.setoid_ring.Ring_polynom.
-(* Kludge for 8.4/8.5 compatibility *)
-Module Import mynsatz_compute.
-  Import Nsatz.
-  Global Ltac mynsatz_compute x := nsatz_compute x.
-End mynsatz_compute.
-Ltac nsatz_compute x := mynsatz_compute x.
-
-Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens :=
-  nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens).
-
-Ltac nsatz_compute_get_leading_coefficient :=
-  lazymatch goal with
-    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a
-  end.
-
-Ltac nsatz_compute_get_certificate :=
-  lazymatch goal with
-    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:((c,b))
-  end.
-
-Ltac nsatz_rewrite_and_revert domain :=
-  lazymatch type of domain with
-  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
-    lazymatch goal with
-    | |- eq _ zero => idtac
-    | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring))
-    end;
-    repeat match goal with
-           | [H : eq _ zero |- _ ] => revert H
-           | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H
-           end
-  end.
-
-(** As per https://coq.inria.fr/bugs/show_bug.cgi?id=4851, [nsatz]
-    cannot handle duplicate hypotheses.  So we clear them. *)
-Ltac nsatz_clear_duplicates_for_bug_4851 domain :=
-  lazymatch type of domain with
-  | @Integral_domain.Integral_domain _ _ _ _ _ _ _ ?eq _ _ _ =>
-    repeat match goal with
-           | [ H : eq ?x ?y, H' : eq ?x ?y |- _ ] => clear H'
-           end
-  end.
-
-Ltac nsatz_nonzero :=
-  try solve [apply Integral_domain.integral_domain_one_zero
-            |apply Integral_domain.integral_domain_minus_one_zero
-            |trivial
-            |assumption].
-
-Ltac nsatz_domain_sugar_power domain sugar power :=
-  let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *)
-  lazymatch type of domain with
-  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
-    nsatz_clear_duplicates_for_bug_4851 domain;
-    nsatz_rewrite_and_revert domain;
-    let reified_package := nsatz_reify_equations eq zero in
-    let fv := nsatz_get_free_variables reified_package in
-    let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in
-    let reified_givens := nsatz_get_reified_givens reified_package in
-    let reified_goal := nsatz_get_reified_goal reified_package in
-    nsatz_compute_to_goal sugar nparams reified_goal power reified_givens;
-    let a := nsatz_compute_get_leading_coefficient in
-    let crt := nsatz_compute_get_certificate in
-    intros _ (* discard [nsatz_compute] output *); intros;
-    apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
-    [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
-    | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *)
-    | solve [repeat (split; [assumption|]); exact I] ]
-  end.
-
-Ltac nsatz_guess_domain :=
-  match goal with
-  | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
-  | |- not (?eq _ _) =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
-  | [H: ?eq _ _ |- _ ] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
-  | [H: not (?eq _ _) |- _] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
-  end.
-
-Ltac nsatz_sugar_power sugar power :=
-  let domain := nsatz_guess_domain in
-  nsatz_domain_sugar_power domain sugar power.
-
-Ltac nsatz_power power :=
-  let power_N := (eval compute in (BinNat.N.of_nat power)) in
-  nsatz_sugar_power BinInt.Z0 power_N.
-
-Ltac nsatz := nsatz_power 1%nat.
-
-Tactic Notation "nsatz" := nsatz.
-Tactic Notation "nsatz" constr(n) := nsatz_power n.
-
-(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y]
-    contradicts any hypothesis of the form [?x' <> ?y'], we turn this
-    problem about inequalities into one about equalities and give it
-    to [nsatz]. *)
-Ltac nsatz_contradict_single_hypothesis domain :=
-  lazymatch type of domain with
-  | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
-    unfold not in *;
-    match goal with
-    | [ H : eq _ _ -> False |- eq _ _ -> False ]
-      => intro; apply H; nsatz
-    | [ H : eq _ _ -> False |- False ]
-      => apply H; nsatz
-    end
-  end.
-
-Ltac nsatz_contradict :=
-  let domain := nsatz_guess_domain in
-  nsatz_contradict_single_hypothesis domain
-  || (unfold not;
-      intros;
-      lazymatch type of domain with
-      | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
-        assert (eq one zero) as Hbad;
-        [nsatz; nsatz_nonzero
-        |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)]
-      end).
diff --git a/src/Tactics/VerdiTactics.v b/src/Tactics/VerdiTactics.v
deleted file mode 100644
index 4060fc675..000000000
--- a/src/Tactics/VerdiTactics.v
+++ /dev/null
@@ -1,414 +0,0 @@
-(*
-Copyright (c) 2014-2015, Verdi Team
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are
-met:
-
-1. Redistributions of source code must retain the above copyright
-notice, this list of conditions and the following disclaimer.
-
-2. Redistributions in binary form must reproduce the above copyright
-notice, this list of conditions and the following disclaimer in the
-documentation and/or other materials provided with the distribution.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
-LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
-A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
-HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
-SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
-LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
-DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
-THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-*)
-
-Ltac subst_max := idtac "VerdiTactics is deprecated in fiat-crypto";
-  repeat match goal with
-           | [ H : ?X = _ |- _ ]  => subst X
-           | [H : _ = ?X |- _] => subst X
-         end.
-
-Ltac inv H := idtac "VerdiTactics is deprecated in fiat-crypto"; inversion H; subst_max.
-Ltac invc H := idtac "VerdiTactics is deprecated in fiat-crypto"; inv H; clear H.
-Ltac invcs H := idtac "VerdiTactics is deprecated in fiat-crypto"; invc H; simpl in *.
-
-Ltac break_if := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ |- context [ if ?X then _ else _ ] ] =>
-      match type of X with
-        | sumbool _ _ => destruct X
-        | _ => destruct X eqn:?
-      end
-    | [ H : context [ if ?X then _ else _ ] |- _] =>
-      match type of X with
-        | sumbool _ _ => destruct X
-        | _ => destruct X eqn:?
-      end
-  end.
-
-Ltac break_match_hyp := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : context [ match ?X with _ => _ end ] |- _] =>
-      match type of X with
-        | sumbool _ _ => destruct X
-        | _ => destruct X eqn:?
-      end
-  end.
-
-Ltac break_match_goal := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ |- context [ match ?X with _ => _ end ] ] =>
-      match type of X with
-        | sumbool _ _ => destruct X
-        | _ => destruct X eqn:?
-      end
-  end.
-
-Ltac break_match := idtac "VerdiTactics is deprecated in fiat-crypto"; break_match_goal || break_match_hyp.
-
-
-Ltac break_exists := idtac "VerdiTactics is deprecated in fiat-crypto";
-  repeat match goal with
-           | [H : exists _, _ |- _ ] => destruct H
-         end.
-
-Ltac break_exists_exists := idtac "VerdiTactics is deprecated in fiat-crypto";
-  repeat match goal with
-           | H:exists _, _ |- _ =>
-             let x := fresh "x" in
-             destruct H as [x]; exists x
-         end.
-
-Ltac break_and := idtac "VerdiTactics is deprecated in fiat-crypto";
-  repeat match goal with
-           | [H : _ /\ _ |- _ ] => destruct H
-         end.
-
-Ltac solve_by_inversion' tac := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [H : _ |- _] => solve [inv H; tac]
-  end.
-
-Ltac solve_by_inversion := idtac "VerdiTactics is deprecated in fiat-crypto"; solve_by_inversion' auto.
-
-Ltac apply_fun f H:= idtac "VerdiTactics is deprecated in fiat-crypto";
-  match type of H with
-    | ?X = ?Y => assert (f X = f Y)
-  end.
-
-Ltac conclude H tac := idtac "VerdiTactics is deprecated in fiat-crypto";
-  (let H' := fresh in
-   match type of H with
-     | ?P -> _ => assert P as H' by (tac)
-   end; specialize (H H'); clear H').
-
-Ltac concludes := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?P -> _ |- _ ] => conclude H auto
-  end.
-
-Ltac forward H := idtac "VerdiTactics is deprecated in fiat-crypto";
-  let H' := fresh in
-   match type of H with
-     | ?P -> _ => assert P as H'
-   end.
-
-Ltac forwards := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?P -> _ |- _ ] => forward H
-  end.
-
-Ltac find_contradiction := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?X = _, H' : ?X = _ |- _ ] => rewrite H in H'; solve_by_inversion
-  end.
-
-Ltac find_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?X _ _ _ _ = _, H' : ?X _ _ _ _ = _ |- _ ] => rewrite H in H'
-    | [ H : ?X = _, H' : ?X = _ |- _ ] => rewrite H in H'
-    | [ H : ?X = _, H' : context [ ?X ] |- _ ] => rewrite H in H'
-    | [ H : ?X = _ |- context [ ?X ] ] => rewrite H
-  end.
-
-Ltac find_rewrite_lem lem := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ |- _ ] =>
-      rewrite lem in H; [idtac]
-  end.
-
-Ltac find_rewrite_lem_by lem t := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ |- _ ] =>
-      rewrite lem in H by t
-  end.
-
-Ltac find_erewrite_lem lem := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ |- _] => erewrite lem in H by eauto
-  end.
-
-Ltac find_reverse_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ = ?X _ _ _ _, H' : ?X _ _ _ _ = _ |- _ ] => rewrite <- H in H'
-    | [ H : _ = ?X, H' : context [ ?X ] |- _ ] => rewrite <- H in H'
-    | [ H : _ = ?X |- context [ ?X ] ] => rewrite <- H
-  end.
-
-Ltac find_inversion := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?X _ _ _ _ _ _ = ?X _ _ _ _ _ _ |- _ ] => invc H
-    | [ H : ?X _ _ _ _ _ = ?X _ _ _ _ _ |- _ ] => invc H
-    | [ H : ?X _ _ _ _ = ?X _ _ _ _ |- _ ] => invc H
-    | [ H : ?X _ _ _ = ?X _ _ _ |- _ ] => invc H
-    | [ H : ?X _ _ = ?X _ _ |- _ ] => invc H
-    | [ H : ?X _ = ?X _ |- _ ] => invc H
-  end.
-
-Ltac prove_eq := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?X ?x1 ?x2 ?x3 = ?X ?y1 ?y2 ?y3 |- _ ] =>
-      assert (x1 = y1) by congruence;
-        assert (x2 = y2) by congruence;
-        assert (x3 = y3) by congruence;
-        clear H
-    | [ H : ?X ?x1 ?x2 = ?X ?y1 ?y2 |- _ ] =>
-      assert (x1 = y1) by congruence;
-        assert (x2 = y2) by congruence;
-        clear H
-    | [ H : ?X ?x1 = ?X ?y1 |- _ ] =>
-      assert (x1 = y1) by congruence;
-        clear H
-  end.
-
-Ltac tuple_inversion := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : (_, _, _, _) = (_, _, _, _) |- _ ] => invc H
-    | [ H : (_, _, _) = (_, _, _) |- _ ] => invc H
-    | [ H : (_, _) = (_, _) |- _ ] => invc H
-  end.
-
-Ltac f_apply H f := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match type of H with
-    | ?X = ?Y =>
-      assert (f X = f Y) by (rewrite H; auto)
-  end.
-
-Ltac break_let := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : context [ (let (_,_) := ?X in _) ] |- _ ] => destruct X eqn:?
-    | [ |- context [ (let (_,_) := ?X in _) ] ] => destruct X eqn:?
-  end.
-
-Ltac break_or_hyp := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ \/ _ |- _ ] => invc H
-  end.
-
-Ltac copy_apply lem H := idtac "VerdiTactics is deprecated in fiat-crypto";
-  let x := fresh in
-  pose proof H as x;
-    apply lem in x.
-
-Ltac copy_eapply lem H := idtac "VerdiTactics is deprecated in fiat-crypto";
-  let x := fresh in
-  pose proof H as x;
-    eapply lem in x.
-
-Ltac conclude_using tac := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?P -> _ |- _ ] => conclude H tac
-  end.
-
-Ltac find_higher_order_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ = _ |- _ ] => rewrite H in *
-    | [ H : forall _, _ = _ |- _ ] => rewrite H in *
-    | [ H : forall _ _, _ = _ |- _ ] => rewrite H in *
-  end.
-
-Ltac find_reverse_higher_order_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ = _ |- _ ] => rewrite <- H in *
-    | [ H : forall _, _ = _ |- _ ] => rewrite <- H in *
-    | [ H : forall _ _, _ = _ |- _ ] => rewrite <- H in *
-  end.
-
-Ltac clean := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?X = ?X |- _ ] => clear H
-  end.
-
-Ltac find_apply_hyp_goal := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ |- _ ] => solve [apply H]
-  end.
-
-Ltac find_copy_apply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ |- _ ] => copy_apply lem H
-  end.
-
-Ltac find_apply_hyp_hyp := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : forall _, _ -> _,
-        H' : _ |- _ ] =>
-      apply H in H'; [idtac]
-    | [ H : _ -> _ , H' : _ |- _ ] =>
-      apply H in H'; auto; [idtac]
-  end.
-
-Ltac find_copy_apply_hyp_hyp := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : forall _, _ -> _,
-        H' : _ |- _ ] =>
-      copy_apply H H'; [idtac]
-    | [ H : _ -> _ , H' : _ |- _ ] =>
-      copy_apply H H'; auto; [idtac]
-  end.
-
-Ltac find_apply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ |- _ ] => apply lem in H
-  end.
-
-Ltac find_eapply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ |- _ ] => eapply lem in H
-  end.
-
-Ltac insterU H := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match type of H with
-    | forall _ : ?T, _ =>
-      let x := fresh "x" in
-      evar (x : T);
-      let x' := (eval unfold x in x) in
-        clear x; specialize (H x')
-  end.
-
-Ltac find_insterU := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : forall _, _ |- _ ] => insterU H
-  end.
-
-Ltac eapply_prop P := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | H : P _ |- _ =>
-      eapply H
-  end.
-
-Ltac isVar t := idtac "VerdiTactics is deprecated in fiat-crypto";
-    match goal with
-      | v : _ |- _ =>
-        match t with
-          | v => idtac
-        end
-    end.
-
-Ltac remGen t := idtac "VerdiTactics is deprecated in fiat-crypto";
-  let x := fresh in
-  let H := fresh in
-  remember t as x eqn:H;
-    generalize dependent H.
-
-Ltac remGenIfNotVar t := idtac "VerdiTactics is deprecated in fiat-crypto"; first [isVar t| remGen t].
-
-Ltac rememberNonVars H := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match type of H with
-    | _ ?a ?b ?c ?d ?e =>
-      remGenIfNotVar a;
-      remGenIfNotVar b;
-      remGenIfNotVar c;
-      remGenIfNotVar d;
-      remGenIfNotVar e
-    | _ ?a ?b ?c ?d =>
-      remGenIfNotVar a;
-      remGenIfNotVar b;
-      remGenIfNotVar c;
-      remGenIfNotVar d
-    | _ ?a ?b ?c =>
-      remGenIfNotVar a;
-      remGenIfNotVar b;
-      remGenIfNotVar c
-    | _ ?a ?b =>
-      remGenIfNotVar a;
-      remGenIfNotVar b
-    | _ ?a =>
-      remGenIfNotVar a
-  end.
-
-Ltac generalizeEverythingElse H := idtac "VerdiTactics is deprecated in fiat-crypto";
-  repeat match goal with
-           | [ x : ?T |- _ ] =>
-             first [
-                 match H with
-                   | x => fail 2
-                 end |
-                 match type of H with
-                   | context [x] => fail 2
-                 end |
-                 revert x]
-         end.
-
-Ltac prep_induction H := idtac "VerdiTactics is deprecated in fiat-crypto";
-  rememberNonVars H;
-  generalizeEverythingElse H.
-
-Ltac econcludes := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?P -> _ |- _ ] => conclude H eauto
-  end.
-
-Ltac find_copy_eapply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : _ |- _ ] => copy_eapply lem H
-  end.
-
-Ltac apply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-  | [ H : context [ P ], H' : context [ Q ] |- _ ] =>
-    apply H in H'
-  end.
-
-
-Ltac eapply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-  | [ H : context [ P ], H' : context [ Q ] |- _ ] =>
-    eapply H in H'
-  end.
-
-Ltac copy_eapply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : context [ P ], H' : context [ Q ] |- _ ] =>
-      copy_eapply H H'
-  end.
-
-Ltac find_false := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | H : _ -> False |- _ => exfalso; apply H
-  end.
-
-Ltac injc H := idtac "VerdiTactics is deprecated in fiat-crypto";
-  injection H; clear H; intro; subst_max.
-
-Ltac find_injection := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-    | [ H : ?X _ _ _ _ _ _ = ?X _ _ _ _ _ _ |- _ ] => injc H
-    | [ H : ?X _ _ _ _ _ = ?X _ _ _ _ _ |- _ ] => injc H
-    | [ H : ?X _ _ _ _ = ?X _ _ _ _ |- _ ] => injc H
-    | [ H : ?X _ _ _ = ?X _ _ _ |- _ ] => injc H
-    | [ H : ?X _ _ = ?X _ _ |- _ ] => injc H
-    | [ H : ?X _ = ?X _ |- _ ] => injc H
-  end.
-
-Ltac aggresive_rewrite_goal := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with H : _ |- _ => rewrite H end.
-
-Ltac break_exists_name x := idtac "VerdiTactics is deprecated in fiat-crypto";
-  match goal with
-  | [ H : exists _, _ |- _ ] => destruct H as [x H]
-  end.