diff options
Diffstat (limited to 'theories/Classes/SetoidAxioms.v')
| -rw-r--r-- | theories/Classes/SetoidAxioms.v | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v deleted file mode 100644 index 03bb9a80..00000000 --- a/theories/Classes/SetoidAxioms.v +++ /dev/null @@ -1,34 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Extensionality axioms that can be used when reasoning with setoids. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud - * 91405 Orsay, France *) - -(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *) - -Require Import Coq.Program.Program. - -Set Implicit Arguments. -Unset Strict Implicit. - -Require Export Coq.Classes.SetoidClass. - -(* Application of the extensionality axiom to turn a goal on - Leibniz equality to a setoid equivalence (use with care!). *) - -Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y. - -(** Application of the extensionality principle for setoids. *) - -Ltac setoid_extensionality := - match goal with - [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y)) - end. |