demo unparallel processing

9785331f · Ralf Jung · 6a39300e · 9785331f
Commit 9785331f authored Jan 17, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

theories/algebra/cmra.v theories/algebra/cmra.v +1 -0

No files found.
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1070,6 +1070,7 @@ Qed.
 Next Obligation. by intros F1 F2 A B [??]; rewrite /= !rFunctor_id. Qed.
 Next Obligation.
  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
+  do 10000 try tauto.
  by rewrite !rFunctor_compose.
 Qed.
 Notation "F1 * F2" := (prodRF F1%RF F2%RF) : rFunctor_scope.