diff options
Diffstat (limited to 'plugins/setoid_ring/Ncring_initial.v')
| -rw-r--r-- | plugins/setoid_ring/Ncring_initial.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 528ad4f17..40748c044 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -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!*) |