aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/ZCoeff.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/ZCoeff.v')
-rw-r--r--plugins/micromega/ZCoeff.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index ced67e39d..f27cd15e3 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -56,7 +56,7 @@ Proof.
destruct sor.(SORsetoid).
apply Equivalence_Transitive.
Qed.
-
+
Add Relation R req
reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)