diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-02 12:48:02 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-02 15:48:09 -0400 |
| commit | 7f20cf022c139dac1379dd249dd9b42998d6aced (patch) | |
| tree | ec326b091999ad3a097c552a8eb0a1be9ba40153 /src/Util/IterAssocOp.v | |
| parent | 2fc3ff8afe6396c2866874980e3721dda2505839 (diff) | |
improve some fragile proofs (built on 8.4)
Diffstat (limited to 'src/Util/IterAssocOp.v')
| -rw-r--r-- | src/Util/IterAssocOp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 773fea8fd..d630698e7 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -243,7 +243,7 @@ Proof. | _ => solve [ reflexivity | congruence | eauto 99 ] | _ => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)))) | _ => progress eapply Proper_test_and_op - | _ => progress eapply conj + | _ => progress split | _ => progress (cbv [fst snd pointwise_relation respectful] in * ) | _ => intro end. |