diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-12 14:09:17 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-12 14:09:17 -0500 |
| commit | edac504b9f30c07e752719b616fe8730b88ff36c (patch) | |
| tree | 5ffa3fc413f90e1726be18ba48d64ac00beed00e /src/EdDSARepChange.v | |
| parent | b86dd1827e7da918148a650cc82d70dacaf3a545 (diff) | |
Fix for Coq 8.4pl2
Diffstat (limited to 'src/EdDSARepChange.v')
| -rw-r--r-- | src/EdDSARepChange.v | 2 |
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 ] |