Merge pull request #665 from ejgallego/protect_recovery_dot

[parsing] Bump Coq to fix lexer error recovery.
ejgallego · Apr 4, 2024 · 516c487 · 516c487
2 parents 50eb3ad + f68390b
commit 516c487
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 2 deletions.
diff --git a/examples/err_shift.v b/examples/err_shift.v
@@ -0,0 +1,9 @@
+Definition map_union_weak `{β A, Insert K A (M A), ∀ A, Empty (M A), ∀ A, 
+   Lookup K A (M A),
+    ∀ A, FinMapToList K A (M A)} {A} (m1 m2 : M A) :=
+  map_imap (λ l v, Some (default v (m1 !! l))) m2.
+
+Section theorems.
+
+Lemma map_union_weak_insert {K A} `{Countable K} (m1 m2 : gmap K A) (i : K) (x : A):
+    map_union_weak (<[i := x]>m1) m2 = alter (λ _, x) i (map_union_weak m1 m2).
diff --git a/vendor/coq b/vendor/coq
diff --git a/vendor/coq-serapi b/vendor/coq-serapi