aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/EdDSARepChange.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/EdDSARepChange.v b/src/EdDSARepChange.v
index 20e544437..d36f07b9b 100644
--- a/src/EdDSARepChange.v
+++ b/src/EdDSARepChange.v
@@ -170,7 +170,7 @@ Section EdDSA.
[ repeat match goal with
| |- _ => intro
| |- _ => eapply Proper_option_rect_nd_changebody
- | |- _ ?x ?x => reflexivity
+ | |- ?R ?x ?x => reflexivity
| H : _ |- _ => rewrite H; reflexivity
end
]