Adapt to Coq PR #17993 fixing Coq bug #12521 about simpl failing on m…

…utual fixpoints with parameters. (#94)
mit-plv · Sep 3, 2023 · ff204c0 · ff204c0
1 parent 2bb593d
commit ff204c0
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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. }