diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-18 14:47:36 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-18 14:47:36 -0700 |
| commit | 90c6403a50addd0cd0775aa45510e78505304017 (patch) | |
| tree | af4fe116033c2a12cdc8cd1364b1437c141d0f75 | |
| parent | d12f190a2ef6f129583f1fd69411638e237d731e (diff) | |
Silence a warning
File "./src/Experiments/GenericFieldPow.v", line 130, characters 4-471:
Warning: Casts are ignored in patterns [cast-in-pattern,automation]
@andres-erbsen Did you intend for the cast at
https://github.com/mit-plv/fiat-crypto/commit/6823b63275333ebb11c7f84068894f76cdb06068#diff-078114b2627a38e74938989c7ca2f6d1R131
to have semantic meaning for some reason, performance or otherwise?
| -rw-r--r-- | src/Experiments/GenericFieldPow.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v index 33d524567..b3d83dbe8 100644 --- a/src/Experiments/GenericFieldPow.v +++ b/src/Experiments/GenericFieldPow.v @@ -129,7 +129,7 @@ Module F. Field_simplify_done : forall (H:x==y), field_simplify_done H. Ltac field_nsatz := repeat match goal with - [ H: (_:F) == _ |- _ ] => + [ H: _ == _ |- _ ] => match goal with | [ Ha : field_simplify_done H |- _ ] => fail | _ => idtac |