diff --git a/src/Parsers/Reachable/ParenBalanced/MinimalOfCore.v b/src/Parsers/Reachable/ParenBalanced/MinimalOfCore.v
index 11064db8..851db61f 100644
--- a/src/Parsers/Reachable/ParenBalanced/MinimalOfCore.v
+++ b/src/Parsers/Reachable/ParenBalanced/MinimalOfCore.v
@@ -305,7 +305,7 @@ Section cfg.
           { left.
             eexists (PBNil _ _ _).
             unfold pb'_productions__of__minimal_pb'_productions; simpl.
-            rewrite expand_size_of_pb'_productions.
+            try rewrite expand_size_of_pb'_productions. (* compensate Coq bug #12521 before its fix in #17993 *)
             simpl_size_of.
             omega. }
           { assert (size_of_pb'_production p0' < h') by exact (lt_helper_1 H_h).
diff --git a/src/Parsers/Reachable/ParenBalancedHiding/MinimalOfCore.v b/src/Parsers/Reachable/ParenBalancedHiding/MinimalOfCore.v
index 304da13d..34621569 100644
--- a/src/Parsers/Reachable/ParenBalancedHiding/MinimalOfCore.v
+++ b/src/Parsers/Reachable/ParenBalancedHiding/MinimalOfCore.v
@@ -342,7 +342,7 @@ Section cfg.
           { left.
             eexists (PBHNil _ _ _ _).
             unfold pbh'_productions__of__minimal_pbh'_productions; simpl.
-            rewrite expand_size_of_pbh'_productions.
+            try rewrite expand_size_of_pbh'_productions. (* compensate Coq bug #12521 before its fix in #17993 *)
             simpl_size_of.
             omega. }
           { assert (size_of_pbh'_production p0' < h') by exact (lt_helper_1 H_h).
diff --git a/src/Parsers/SimpleRecognizerCorrect.v b/src/Parsers/SimpleRecognizerCorrect.v
index c1e5f079..029bae67 100644
--- a/src/Parsers/SimpleRecognizerCorrect.v
+++ b/src/Parsers/SimpleRecognizerCorrect.v
@@ -177,6 +177,7 @@ Section convenience.
   Proof.
     pose proof (parse_nonterminal_correct (gcdata := simple_gencdata1) str nt).
     pose proof (parse_nonterminal_correct (gcdata := simple_gencdata2) str nt).
+    Opaque simple_parse_of_item_correct.
     t_parse_correct.
     match goal with H : _ |- _ => rewrite to_of_nonterminal in H end.
     { assumption. }