diff options
| author |  Jason Gross <jagro@google.com> | 2018-06-29 22:31:01 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-07-03 19:28:55 -0400 |
| commit | 031f4cbfc5b2a300e95eb821aa42e72c851c1e59 (patch) | |
| tree | e1682a090b6b74b49a28173df62b0ad0ed049e6a /src | |
| parent | ddc544fbab04ea9abf3ae759bd9ca60b6258b834 (diff) | |
Fix hints, hopefully
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 08637d794..154951973 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -269,7 +269,7 @@ Module Associational. induction p; cbn [flat_map partition fst snd]; eta_expand; break_match; cbn [fst snd]; push; nsatz. Qed. - Hint Rewrite eval_flat_map_if : push_eval. + (*Local Hint Rewrite eval_flat_map_if : push_eval.*) (* this should be [Local], but that doesn't work *) Lemma eval_if (b : bool) p q : eval (if b then p else q) = if b then eval p else eval q. Proof. case b; reflexivity. Qed. |