diff options
Diffstat (limited to 'plugins/setoid_ring/Ncring_initial.v')
| -rw-r--r-- | plugins/setoid_ring/Ncring_initial.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 516a993e..c40e0ffb 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -192,6 +192,7 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x]. Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. Proof. intros;subst;reflexivity. Qed. +Declare Equivalent Keys bracket gen_phiZ. (*proof that [.] satisfies morphism specifications*) Global Instance gen_phiZ_morph : (@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*) |