diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Classes/SetoidAxioms.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
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. |