From 90c6403a50addd0cd0775aa45510e78505304017 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 18 Jul 2016 14:47:36 -0700
Subject: 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?
---
 src/Experiments/GenericFieldPow.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3