diff options
| author | Pierre-Marie Pédrot | 2019-03-31 23:01:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-31 23:01:41 +0200 |
| commit | cb502e44aac8328ffd6c37429e050a01f72b2c53 (patch) | |
| tree | 9d8f62a6b86af6d1eb233c199ab5cc5416834e6e /plugins/setoid_ring/InitialRing.v | |
| parent | 44e5afe99d8b40c3ed0d546f56a446427c7c4da4 (diff) | |
| parent | 3fdb62dee9830bb551798ee9c3dd2a3af1493e8d (diff) | |
Merge PR #8829: Error when [foo.(bar)] is used with nonprojection [bar], warn if [bar] nonprimitive projection.
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/setoid_ring/InitialRing.v')
| -rw-r--r-- | plugins/setoid_ring/InitialRing.v | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 15d490a6ab..4886c8b9aa 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -51,9 +51,9 @@ Section ZMORPHISM. Notation "x == y" := (req x y). Variable Rsth : Setoid_Theory R req. Add Parametric Relation : R req - reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) - symmetry proved by Rsth.(@Equivalence_Symmetric _ _) - transitivity proved by Rsth.(@Equivalence_Transitive _ _) + reflexivity proved by (@Equivalence_Reflexive _ _ Rsth) + symmetry proved by (@Equivalence_Symmetric _ _ Rsth) + transitivity proved by (@Equivalence_Transitive _ _ Rsth) as R_setoid3. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. @@ -267,9 +267,9 @@ Section NMORPHISM. Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). Variable Rsth : Setoid_Theory R req. Add Parametric Relation : R req - reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) - symmetry proved by Rsth.(@Equivalence_Symmetric _ _) - transitivity proved by Rsth.(@Equivalence_Transitive _ _) + reflexivity proved by (@Equivalence_Reflexive _ _ Rsth) + symmetry proved by (@Equivalence_Symmetric _ _ Rsth) + transitivity proved by (@Equivalence_Transitive _ _ Rsth) as R_setoid4. Ltac rrefl := gen_reflexivity Rsth. Variable SReqe : sring_eq_ext radd rmul req. @@ -392,9 +392,9 @@ Section NWORDMORPHISM. Notation "x == y" := (req x y). Variable Rsth : Setoid_Theory R req. Add Parametric Relation : R req - reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) - symmetry proved by Rsth.(@Equivalence_Symmetric _ _) - transitivity proved by Rsth.(@Equivalence_Transitive _ _) + reflexivity proved by (@Equivalence_Reflexive _ _ Rsth) + symmetry proved by (@Equivalence_Symmetric _ _ Rsth) + transitivity proved by (@Equivalence_Transitive _ _ Rsth) as R_setoid5. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. @@ -581,9 +581,9 @@ Section GEN_DIV. (* Useful tactics *) Add Parametric Relation : R req - reflexivity proved by Rsth.(@Equivalence_Reflexive _ _) - symmetry proved by Rsth.(@Equivalence_Symmetric _ _) - transitivity proved by Rsth.(@Equivalence_Transitive _ _) + reflexivity proved by (@Equivalence_Reflexive _ _ Rsth) + symmetry proved by (@Equivalence_Symmetric _ _ Rsth) + transitivity proved by (@Equivalence_Transitive _ _ Rsth) as R_set1. Ltac rrefl := gen_reflexivity Rsth. Add Morphism radd with signature (req ==> req ==> req) as radd_ext. @@ -614,7 +614,7 @@ Section GEN_DIV. Proof. constructor. intros a b;unfold triv_div. - assert (X:= morph.(morph_eq) a b);destruct (ceqb a b). + assert (X:= morph_eq morph a b);destruct (ceqb a b). Esimpl. rewrite X; trivial. rsimpl. |