From c4ce787fddb5d8eefd96cd4706aa1ee7a8ea8843 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 2 Apr 2017 11:01:14 -0400 Subject: Remove coqprime-8.4 We're using tactics in terms in some places, and so have no hope of compiling with Coq 8.4. We no longer pretend to support it. We can probably also remove some other compatibility things, if we want. --- coqprime-8.4/Coqprime/Tactic.v | 84 ------------------------------------------ 1 file changed, 84 deletions(-) delete mode 100644 coqprime-8.4/Coqprime/Tactic.v (limited to 'coqprime-8.4/Coqprime/Tactic.v') diff --git a/coqprime-8.4/Coqprime/Tactic.v b/coqprime-8.4/Coqprime/Tactic.v deleted file mode 100644 index 93a244149..000000000 --- a/coqprime-8.4/Coqprime/Tactic.v +++ /dev/null @@ -1,84 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - - -(********************************************************************** - Tactic.v - Useful tactics - **********************************************************************) - -(************************************** - A simple tactic to end a proof -**************************************) -Ltac finish := intros; auto; trivial; discriminate. - - -(************************************** - A tactic for proof by contradiction - with contradict H - H: ~A |- B gives |- A - H: ~A |- ~ B gives H: B |- A - H: A |- B gives |- ~ A - H: A |- B gives |- ~ A - H: A |- ~ B gives H: A |- ~ A -**************************************) - -Ltac contradict name := - let term := type of name in ( - match term with - (~_) => - match goal with - |- ~ _ => let x := fresh in - (intros x; case name; - generalize x; clear x name; - intro name) - | |- _ => case name; clear name - end - | _ => - match goal with - |- ~ _ => let x := fresh in - (intros x; absurd term; - [idtac | exact name]; generalize x; clear x name; - intros name) - | |- _ => generalize name; absurd term; - [idtac | exact name]; clear name - end - end). - - -(************************************** - A tactic to do case analysis keeping the equality -**************************************) - -Ltac case_eq name := - generalize (refl_equal name); pattern name at -1 in |- *; case name. - - -(************************************** - A tactic to use f_equal? theorems -**************************************) - -Ltac eq_tac := - match goal with - |- (?g _ = ?g _) => apply f_equal with (f := g) - | |- (?g ?X _ = ?g ?X _) => apply f_equal with (f := g X) - | |- (?g _ _ = ?g _ _) => apply f_equal2 with (f := g) - | |- (?g ?X ?Y _ = ?g ?X ?Y _) => apply f_equal with (f := g X Y) - | |- (?g ?X _ _ = ?g ?X _ _) => apply f_equal2 with (f := g X) - | |- (?g _ _ _ = ?g _ _ _) => apply f_equal3 with (f := g) - | |- (?g ?X ?Y ?Z _ = ?g ?X ?Y ?Z _) => apply f_equal with (f := g X Y Z) - | |- (?g ?X ?Y _ _ = ?g ?X ?Y _ _) => apply f_equal2 with (f := g X Y) - | |- (?g ?X _ _ _ = ?g ?X _ _ _) => apply f_equal3 with (f := g X) - | |- (?g _ _ _ _ _ = ?g _ _ _ _) => apply f_equal4 with (f := g) - end. - -(************************************** - A stupid tactic that tries auto also after applying sym_equal -**************************************) - -Ltac sauto := (intros; apply sym_equal; auto; fail) || auto. -- cgit v1.2.3