From 182bc3d1c4540ab1d0dce301bc725e4f9e97efba Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Tue, 28 Jul 2026 04:37:14 +0000
Subject: [PATCH 1/6] Port matching-logic library toward Rocq dev

---
 matching-logic/dune-project                   |  2 +
 .../src/Experimental/ProofModePattern.v       |  4 +-
 matching-logic/src/FreshnessManager.v         |  8 ++--
 matching-logic/src/Pattern.v                  |  7 ++-
 matching-logic/src/Utils/stdpp_ext.v          | 48 ++++++++++---------
 5 files changed, 38 insertions(+), 31 deletions(-)

diff --git a/matching-logic/dune-project b/matching-logic/dune-project
index a45003a3..67682167 100644
--- a/matching-logic/dune-project
+++ b/matching-logic/dune-project
@@ -1,3 +1,5 @@
 (lang dune 2.5)
 (using coq 0.2)
 (name coq-matching-logic)
+(package
+ (name coq-matching-logic))
diff --git a/matching-logic/src/Experimental/ProofModePattern.v b/matching-logic/src/Experimental/ProofModePattern.v
index ff11a1b7..c9504601 100644
--- a/matching-logic/src/Experimental/ProofModePattern.v
+++ b/matching-logic/src/Experimental/ProofModePattern.v
@@ -450,7 +450,7 @@ Section sec.
             simp PMPattern_size.
             rewrite PMPattern_size_clause_2_PMPattern_size_vec_spec.
             remember (vec_to_list args) as args'.
-            apply elem_of_list_lookup_1 in pf.
+            apply list_elem_of_lookup_1 in pf.
             destruct pf as [i Hi].
             pose proof (Hargs := take_drop_middle args' i p Hi).
             subst.
@@ -1271,4 +1271,4 @@ Section sec.
 
     End examples.
 
-End sec.
\ No newline at end of file
+End sec.
diff --git a/matching-logic/src/FreshnessManager.v b/matching-logic/src/FreshnessManager.v
index 35881fa7..8263f942 100644
--- a/matching-logic/src/FreshnessManager.v
+++ b/matching-logic/src/FreshnessManager.v
@@ -686,7 +686,7 @@ Proof.
     pose proof (fm_evars_nodup _ _ _ _ _ FM).
     clear-H.
     intro.
-    apply elem_of_list_lookup_1 in H0 as [i H0].
+    apply list_elem_of_lookup_1 in H0 as [i H0].
     by specialize (H 0 (S i) x x eq_refl H0 ltac:(lia)).
   }
   split.
@@ -694,7 +694,7 @@ Proof.
     pose proof (fm_avoids_evar _ _ _ _ _ FM).
     clear -H.
     intro.
-    apply elem_of_list_lookup_1 in H0 as [i H0].
+    apply list_elem_of_lookup_1 in H0 as [i H0].
     by specialize (H i 0 x x H0 eq_refl).
   }
   {
@@ -747,7 +747,7 @@ Proof.
     pose proof (fm_svars_nodup _ _ _ _ _ FM).
     clear-H.
     intro.
-    apply elem_of_list_lookup_1 in H0 as [i H0].
+    apply list_elem_of_lookup_1 in H0 as [i H0].
     by specialize (H 0 (S i) X X eq_refl H0 ltac:(lia)).
   }
   split.
@@ -755,7 +755,7 @@ Proof.
     pose proof (fm_avoids_svar _ _ _ _ _ FM).
     clear -H.
     intro.
-    apply elem_of_list_lookup_1 in H0 as [i H0].
+    apply list_elem_of_lookup_1 in H0 as [i H0].
     by specialize (H i 0 X X H0 eq_refl).
   }
   {
diff --git a/matching-logic/src/Pattern.v b/matching-logic/src/Pattern.v
index 26fa9011..2a5b02e2 100644
--- a/matching-logic/src/Pattern.v
+++ b/matching-logic/src/Pattern.v
@@ -162,7 +162,10 @@ Section syntax.
       free_evars (foldr patt_imp g l) =
       free_evars g ∪ free_evars_of_list l.
   Proof.
-    induction l; intro g; set_solver.
+    induction l; intro g; simpl.
+    - rewrite union_empty_r_L. reflexivity.
+    - rewrite IHl. apply set_eq. intros x.
+      rewrite !elem_of_union. tauto.
   Qed.
 
   (* for bound set variables *)
@@ -1020,7 +1023,7 @@ Defined.
 
 Global Instance wfPattern_countable {Σ : Signature} : Countable wfPattern.
 Proof.
-  apply countable_sig.
+  apply sig_countable.
   solve_decision.
 Defined.
 
diff --git a/matching-logic/src/Utils/stdpp_ext.v b/matching-logic/src/Utils/stdpp_ext.v
index ecdc0f49..1ae60858 100644
--- a/matching-logic/src/Utils/stdpp_ext.v
+++ b/matching-logic/src/Utils/stdpp_ext.v
@@ -3,6 +3,8 @@ From Coq Require Export ssreflect ssrfun ssrbool String.
 From Coq.Logic Require Import Classical_Prop Classical_Pred_Type Eqdep_dec.
 From stdpp Require Export list propset sets pmap gmap mapset coGset.
 Export list. (* to overwrite module qualifiers *)
+From stdpp Require Import list.
+Definition option_last {A} : list A -> option A := @last A.
 
 Lemma foldl_fold_left :
   forall {A B} f (l : list A) (b : B),
@@ -84,9 +86,9 @@ Proof.
   { reflexivity. }
   rewrite -> Hk at 1.
   split; intros H'.
-  + apply elem_of_list_fmap_2_inj in H'. apply H'.
-    apply inj_unit_r.
-  + apply elem_of_list_fmap_1. assumption.
+  + apply list_elem_of_fmap in H' as [[k' []] [Hkk' H']].
+    simpl in Hkk'. subst k'. exact H'.
+  + apply list_elem_of_fmap_2. assumption.
 Qed.
 
 Lemma mapset_elements_to_set `{Countable K} (X : gset K) : list_to_set (mapset_elements X) = X.
@@ -119,7 +121,7 @@ Qed.
 
 (* [1,2,3,4,5] -> [5,4,3,2,1] -> [4,3,2,1] -> [1,2,3,4] *)
 Lemma rev_tail_rev_app_last A (l : list A) (xlast : A):
-  stdpp.list.last l = Some xlast ->
+  option_last l = Some xlast ->
   (rev (tail (rev l)) ++ [xlast]) = l.
 Proof.        
   move: xlast.
@@ -167,7 +169,7 @@ Proof.
 Qed.
 
 
-Lemma last_rev_head A (l : list A) (x : A) : stdpp.list.last (x :: l) = hd_error (rev l ++ [x]).
+Lemma last_rev_head A (l : list A) (x : A) : option_last (x :: l) = hd_error (rev l ++ [x]).
 Proof.
   remember (length l) as len.
   assert (Hlen: length l <= len).
@@ -186,7 +188,7 @@ Proof.
 Qed.
 
 (* The same lemma for stdpp's `reverse *)
-Lemma last_reverse_head A (l : list A) (x : A) : stdpp.list.last (x :: l) = hd_error (reverse l ++ [x]).
+Lemma last_reverse_head A (l : list A) (x : A) : option_last (x :: l) = hd_error (reverse l ++ [x]).
 Proof.
   remember (length l) as len.
   assert (Hlen: length l <= len).
@@ -247,10 +249,11 @@ Definition tail_skip_eq {A} {eqdec: EqDecision A} (l : list (A * A)) :=
   reverse (skip_eq (reverse l)).
 
 Lemma tail_skip_eq_last_not_eq {A} {eqdec: EqDecision A} (l : list (A * A)) :
-  ∀ x y, stdpp.list.last (tail_skip_eq l) = Some (x, y) -> x <> y.
+  ∀ x y, option_last (tail_skip_eq l) = Some (x, y) -> x <> y.
 Proof.
   intros x y H.
   unfold tail_skip_eq in H.
+  unfold option_last in H.
   rewrite last_reverse in H.
   apply skip_eq_head_not_eq in H.
   apply H.
@@ -294,7 +297,7 @@ Abort.
 
 Lemma common_length_rev {A} {eqdec: EqDecision A} (x y : A) (xs ys : list A) :
   common_length (reverse (x::xs)) (y::ys) =
-  match (decide ((stdpp.list.last (x::xs)) = Some y)) with
+  match (decide ((option_last (x::xs)) = Some y)) with
   | left _ => S (common_length (reverse (tail (reverse (x::xs)))) ys)
   | right _ => 0
   end.
@@ -307,7 +310,7 @@ Proof.
 Abort.
 
 Lemma last_app_singleton {A} (m : A) (l : list A) :
-  stdpp.list.last (l ++ [m]) = Some m.
+  option_last (l ++ [m]) = Some m.
 Proof.
   induction l.
   - reflexivity.
@@ -333,24 +336,24 @@ Proof.
     move: ys H.
     induction xs as [|x xs]; intros ys H.
     + rewrite zip_with_nil_r.
-      apply stdpp.list.Forall_nil.
+      apply Forall_nil.
       exact I.
     + destruct ys as [|y ys].
-      { simpl. apply stdpp.list.Forall_nil. exact I. }
+      { simpl. apply Forall_nil. exact I. }
       simpl in H. simpl.
       inversion H. subst. simpl in H2.
-      apply stdpp.list.Forall_cons. split.
+      apply Forall_cons. split.
       { simpl. apply H2. }
       apply IHxs. apply H3.
   - intros H.
     move: ys H.
     induction xs as [|x xs]; intros ys H.
-    + simpl. apply stdpp.list.Forall_nil. exact I.
+    + simpl. apply Forall_nil. exact I.
     + destruct ys as [|y ys].
-      { simpl. apply stdpp.list.Forall_nil. exact I. }
+      { simpl. apply Forall_nil. exact I. }
       simpl in H. simpl.
       inversion H. subst. simpl in H2.
-      apply stdpp.list.Forall_cons. split.
+      apply Forall_cons. split.
       { simpl. apply H2. }
       apply IHxs. apply H3.
 Qed.
@@ -513,17 +516,17 @@ Proof.
     { rewrite drop_nil. apply H. }
     simpl in Hlen. lia.
   - destruct l as [|x l], n.
-    { simpl. apply stdpp.list.Forall_nil. exact I. }
-    { rewrite drop_nil. apply stdpp.list.Forall_nil. exact I. }
+    { simpl. apply Forall_nil. exact I. }
+    { rewrite drop_nil. apply Forall_nil. exact I. }
     { simpl. apply H. }
     simpl. apply IHlen. simpl in Hlen. lia.
     inversion H. assumption.
 Qed.
 
 Lemma last_drop {A : Type} (l : list A) (n : nat) (x : A) :
-  stdpp.list.last l = Some x ->
+  option_last l = Some x ->
   n < length l ->
-  stdpp.list.last (drop n l) = Some x.
+  option_last (drop n l) = Some x.
 Proof.
   remember (length l) as len.
   assert (Hlen: length l <= len).
@@ -629,7 +632,7 @@ Proof.
 Qed.
 
 Lemma list_last_length {A : Type} (l : list A):
-  stdpp.list.last l = l !! (length l - 1).
+  option_last l = l !! (length l - 1).
 Proof.
   remember (length l) as len.
   rewrite Heqlen.
@@ -682,9 +685,9 @@ Proof.
 Qed.
 
 Lemma last_tail {A : Type} (l : list A) (lst m : A) :
-  stdpp.list.last l = Some lst ->
+  option_last l = Some lst ->
   head (tail l) = Some m ->
-  stdpp.list.last (tail l) = Some lst.
+  option_last (tail l) = Some lst.
 Proof.
   remember (length l) as len.
   assert (Hlen: length l <= len).
@@ -1140,4 +1143,3 @@ Lemma propset_top_elem_of {A}:
 Proof.
   set_solver.
 Qed.
-

From c3c581988699d7d0e7a07dd8eb39375c35543495 Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Tue, 28 Jul 2026 05:49:54 +0000
Subject: [PATCH 2/6] Advance Matching Logic build with Rocq dev

---
 matching-logic/src/FreshnessManager.v | 32 ++++++++++++------------
 matching-logic/src/PrePredicate.v     | 16 ++++++------
 matching-logic/src/ProofSystem.v      |  2 +-
 matching-logic/src/Syntax.v           | 35 +++++++++++++++++++++------
 4 files changed, 53 insertions(+), 32 deletions(-)

diff --git a/matching-logic/src/FreshnessManager.v b/matching-logic/src/FreshnessManager.v
index 8263f942..a4c7d56c 100644
--- a/matching-logic/src/FreshnessManager.v
+++ b/matching-logic/src/FreshnessManager.v
@@ -261,7 +261,7 @@ Proof.
             subst y0.
             apply nesym.
             apply He0.
-            rewrite elem_of_list_lookup.
+            rewrite list_elem_of_lookup.
             exists i.
             exact Hi.
         }
@@ -285,14 +285,14 @@ Proof.
         {
             inversion Hi. subst x0.
             apply He2.
-            eapply elem_of_list_lookup_2.
+            eapply list_elem_of_lookup_2.
             apply Hj.
         }
         {
             inversion Hj. subst y0.
             apply nesym.
             apply He2.
-            eapply elem_of_list_lookup_2.
+            eapply list_elem_of_lookup_2.
             apply Hi.
         }
         {
@@ -321,12 +321,12 @@ Proof.
             }
             assert (Hϕinfmp: ϕ ∈ avoided_patterns).
             {
-                apply elem_of_list_lookup.
+                apply list_elem_of_lookup.
                 exists j. apply Hj.
             }
             clear Hj.
             subst evs.
-            setoid_rewrite elem_of_list_join in He1.
+            setoid_rewrite list_elem_of_join in He1.
             specialize (He1 x).
             apply He1.
             2: reflexivity.
@@ -337,11 +337,11 @@ Proof.
             }
             subst llevs.
             unfold fmap.
-            rewrite elem_of_list_fmap.
+            rewrite list_elem_of_fmap.
             eexists. split. reflexivity.
             subst levs.
             unfold fmap.
-            rewrite elem_of_list_fmap.
+            rewrite list_elem_of_fmap.
             eexists. split. reflexivity.
             exact Hϕinfmp.
         }
@@ -439,7 +439,7 @@ Proof.
             subst y0.
             apply nesym.
             apply He0.
-            rewrite elem_of_list_lookup.
+            rewrite list_elem_of_lookup.
             exists i.
             exact Hi.
         }
@@ -463,14 +463,14 @@ Proof.
         {
             inversion Hi. subst x0.
             apply He2.
-            eapply elem_of_list_lookup_2.
+            eapply list_elem_of_lookup_2.
             apply Hj.
         }
         {
             inversion Hj. subst y0.
             apply nesym.
             apply He2.
-            eapply elem_of_list_lookup_2.
+            eapply list_elem_of_lookup_2.
             apply Hi.
         }
         {
@@ -499,12 +499,12 @@ Proof.
             }
             assert (Hϕinfmp: ϕ ∈ avoided_patterns).
             {
-                apply elem_of_list_lookup.
+                apply list_elem_of_lookup.
                 exists j. apply Hj.
             }
             clear Hj.
             subst svs.
-            setoid_rewrite elem_of_list_join in He1.
+            setoid_rewrite list_elem_of_join in He1.
             specialize (He1 X).
             apply He1.
             2: reflexivity.
@@ -515,11 +515,11 @@ Proof.
             }
             subst llsvs.
             unfold fmap.
-            rewrite elem_of_list_fmap.
+            rewrite list_elem_of_fmap.
             eexists. split. reflexivity.
             subst lsvs.
             unfold fmap.
-            rewrite elem_of_list_fmap.
+            rewrite list_elem_of_fmap.
             eexists. split. reflexivity.
             exact Hϕinfmp.
         }
@@ -605,7 +605,7 @@ Proof.
     {
         rewrite elem_of_disjoint.
         intros x Hx HContra.
-        rewrite elem_of_list_lookup in Hx.
+        rewrite list_elem_of_lookup in Hx.
         destruct Hx as [i Hx].
         destruct FM.
         assert (H : evar_is_fresh_in x ap).
@@ -622,7 +622,7 @@ Proof.
     {
         rewrite elem_of_disjoint.
         intros x Hx HContra.
-        rewrite elem_of_list_lookup in Hx.
+        rewrite list_elem_of_lookup in Hx.
         destruct Hx as [i Hx].
         destruct FM.
         assert (H : svar_is_fresh_in x ap).
diff --git a/matching-logic/src/PrePredicate.v b/matching-logic/src/PrePredicate.v
index 5c5018c3..6f10ef74 100644
--- a/matching-logic/src/PrePredicate.v
+++ b/matching-logic/src/PrePredicate.v
@@ -38,7 +38,7 @@ Section with_signature.
     intros H l Hl Hci Hwf.
     apply H.
     { clear -Hl. induction l. by apply Forall_nil. inversion Hl. subst.
-      apply Forall_cons; split. lia. apply IHl. assumption.
+      apply Forall_cons. lia. apply IHl. assumption.
     }
     { exact Hci. }
     { exact Hwf. }
@@ -720,7 +720,7 @@ Section with_signature.
           simpl in H0.
           inversion Hci; subst.
           {
-            apply Forall_cons; split.
+            apply Forall_cons.
             simpl. inversion H0. subst. simpl in *.
             lia. by apply Forall_nil.
           }
@@ -729,7 +729,7 @@ Section with_signature.
             inversion H0. subst. clear H0. simpl in *.
             specialize (IHl (k1,x1) erefl). simpl in IHl.
             specialize (IHl ltac:(lia)).
-            apply Forall_cons; split.
+            apply Forall_cons.
             {
               simpl. lia.
             }
@@ -847,7 +847,7 @@ Section with_signature.
         by apply Forall_nil.
       }
       {
-        apply Forall_cons; split.
+        apply Forall_cons.
         { lia. }
         apply IHHzeros.
       }
@@ -970,14 +970,14 @@ Section with_signature.
     rewrite bcmcloseex_propagate_last_zero.
     apply H.
     {
-      apply Forall_cons; split. simpl;lia.
+      apply Forall_cons. simpl;lia.
       clear -Hk.
       induction Hk.
       {
         by apply Forall_nil.
       }
       {
-        apply Forall_cons; split. lia. assumption.
+        apply Forall_cons. lia. assumption.
       }
     }
     {
@@ -1088,7 +1088,7 @@ Section with_signature.
     replace (bcmcloseex l (ϕ^{evar: 0 ↦ x}))
     with (bcmcloseex ((0,x)::l) ϕ) by reflexivity.
     apply H with (k := dbi').
-    { apply Forall_cons; split. simpl. lia. assumption. }
+    { apply Forall_cons. simpl. lia. assumption. }
     {
       destruct l.
       { apply ci_single. }
@@ -1099,4 +1099,4 @@ Section with_signature.
     }
   Qed.
 
-End with_signature.
\ No newline at end of file
+End with_signature.
diff --git a/matching-logic/src/ProofSystem.v b/matching-logic/src/ProofSystem.v
index 69429a78..a09295e3 100644
--- a/matching-logic/src/ProofSystem.v
+++ b/matching-logic/src/ProofSystem.v
@@ -131,7 +131,7 @@ Section ml_proof_system.
     Γ ⊢H ϕ -> well_formed ϕ.
   Proof.
     intros pf.
-    induction pf; wf_auto2.
+    induction pf. all: solve [wf_auto2].
   Qed.
 
   Lemma cast_proof {Γ} {ϕ} {ψ} (e : ψ = ϕ) : ML_proof_system Γ ϕ -> ML_proof_system Γ ψ.
diff --git a/matching-logic/src/Syntax.v b/matching-logic/src/Syntax.v
index a4f54661..4a16d77c 100644
--- a/matching-logic/src/Syntax.v
+++ b/matching-logic/src/Syntax.v
@@ -992,9 +992,10 @@ Section with_signature.
   - destruct H as [H _]. exact H.
   - unfold evar_is_fresh_in_list,evar_is_fresh_in in *. simpl in *.
     split;[set_solver|].
-    apply Forall_cons.
     destruct IHl as [IHl1 IHl2].
-    set_solver.
+    apply Forall_cons.
+    + set_solver.
+    + apply IHl1. set_solver.
   - unfold evar_is_fresh_in_list,evar_is_fresh_in in *. simpl in *.
     destruct IHl as [IHl1 IHl2].
     destruct H as [H1 H2].
@@ -2962,11 +2963,31 @@ Section with_signature.
       reflexivity.
       case_match. lia. reflexivity.
     * rewrite negb_or. rewrite negb_or in H0.
-      rewrite IHφ1. 1-3: wf_auto2.
-      rewrite IHφ2; wf_auto2.
+      assert (Hφ1 : ~~ bsvar_occur (bsvar_subst ψ x φ1) dbi).
+      { apply IHφ1.
+        - wf_auto2.
+        - wf_auto2.
+        - wf_auto2. }
+      assert (Hφ2 : ~~ bsvar_occur (bsvar_subst ψ x φ2) dbi).
+      { apply IHφ2.
+        - wf_auto2.
+        - wf_auto2.
+        - wf_auto2. }
+      rewrite Hφ1. rewrite Hφ2.
+      reflexivity.
     * rewrite negb_or. rewrite negb_or in H0.
-      rewrite IHφ1. 1-3: wf_auto2.
-      rewrite IHφ2; wf_auto2.
+      assert (Hφ1 : ~~ bsvar_occur (bsvar_subst ψ x φ1) dbi).
+      { apply IHφ1.
+        - wf_auto2.
+        - wf_auto2.
+        - wf_auto2. }
+      assert (Hφ2 : ~~ bsvar_occur (bsvar_subst ψ x φ2) dbi).
+      { apply IHφ2.
+        - wf_auto2.
+        - wf_auto2.
+        - wf_auto2. }
+      rewrite Hφ1. rewrite Hφ2.
+      reflexivity.
     * rewrite IHφ; wf_auto2.
     * rewrite IHφ; wf_auto2.
   Qed.
@@ -3081,4 +3102,4 @@ Hint Resolve wfc_ex_aux_bevar_subst : core.
 Hint Resolve wfp_svar_open : core.
 
 #[export]
- Hint Resolve wfc_mu_free_evar_subst : core.
\ No newline at end of file
+ Hint Resolve wfc_mu_free_evar_subst : core.

From 7db02dbf7e2efb33a8f3f9fb6329a9c70ad65308 Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Tue, 28 Jul 2026 06:17:46 +0000
Subject: [PATCH 3/6] Adapt core proofs to Rocq dev

---
 matching-logic/src/BasicProofSystemLemmas.v   | 20 ++++++++++---------
 matching-logic/src/ProofMode/Basics.v         |  2 +-
 matching-logic/src/Theories/Bool_Semantics.v  |  4 ++--
 matching-logic/src/Theories/ProductSort.v     |  4 ++--
 matching-logic/src/Theories/Sorts_Semantics.v | 13 ++++++++++--
 matching-logic/src/Theories/SumSort_Syntax.v  |  4 ++--
 matching-logic/src/Utils/stdpp_ext.v          |  4 ++--
 7 files changed, 31 insertions(+), 20 deletions(-)

diff --git a/matching-logic/src/BasicProofSystemLemmas.v b/matching-logic/src/BasicProofSystemLemmas.v
index a7f5566b..7f516cca 100644
--- a/matching-logic/src/BasicProofSystemLemmas.v
+++ b/matching-logic/src/BasicProofSystemLemmas.v
@@ -233,17 +233,18 @@ Proof.
            ++ eapply MP.
               ** eapply MP.
                  --- apply(P2 _ A B C ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
-                 --- unshelve (eapply(P1 _ _ (A ---> B ---> C) _ _)); wf_auto2.
-              ** apply P2; wf_auto2.
+                 --- unshelve (eapply(P1 _ _ (A ---> B ---> C) _ _)).
+                     all: solve [wf_auto2].
+              ** apply P2. all: solve [wf_auto2].
         -- eapply MP.
            ++ apply t1.
            ++ apply(P2 _ ABC ((A ---> B) ---> (A ---> C)) (B ---> (A ---> B) ---> (A ---> C)) ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
       * eapply MP.
         -- eapply MP.
            ++ apply(P2 _ B (A ---> B) (A ---> C) ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
-           ++ apply(P1 _ _ ABC); wf_auto2.
-        -- apply P2; wf_auto2.
-    + apply P2; wf_auto2.
+           ++ apply(P1 _ _ ABC). all: solve [wf_auto2].
+        -- apply P2. all: solve [wf_auto2].
+    + apply P2. all: solve [wf_auto2].
 Defined.
 
 Lemma reorder_meta {Σ : Signature} {Γ : Theory} {A B C : Pattern} {i : ProofInfo} :
@@ -269,12 +270,13 @@ Proof.
   intros WFA WFB WFC.
   apply reorder_meta;[wf_auto2|wf_auto2|wf_auto2|].
   eapply MP.
-  - apply(P1 _ (B ---> C) A); wf_auto2.
+  - apply(P1 _ (B ---> C) A). all: solve [wf_auto2].
   - eapply MP.
     + eapply MP.
-      * apply (P2 _ A B C); wf_auto2.
-      * apply (P1 _ ((A ---> B ---> C) ---> (A ---> B) ---> A ---> C) (B ---> C)); wf_auto2.
-    + apply P2; wf_auto2.
+      * apply (P2 _ A B C). all: solve [wf_auto2].
+      * apply (P1 _ ((A ---> B ---> C) ---> (A ---> B) ---> A ---> C) (B ---> C)).
+        all: solve [wf_auto2].
+    + apply P2. all: solve [wf_auto2].
 Defined.
 
 Lemma syllogism_meta {Σ : Signature} {Γ : Theory} {A B C : Pattern} {i : ProofInfo} :
diff --git a/matching-logic/src/ProofMode/Basics.v b/matching-logic/src/ProofMode/Basics.v
index 2d6b1e2a..6bc1fc39 100644
--- a/matching-logic/src/ProofMode/Basics.v
+++ b/matching-logic/src/ProofMode/Basics.v
@@ -39,7 +39,7 @@ Proof.
 Defined.
 
 Definition find_hyp {Σ : Signature} (name : string) (hyps : hypotheses) : option (nat * named_hypothesis)%type
-:= stdpp.list.list_find (has_name name) hyps.
+:= list_find (has_name name) hyps.
 
 
 Record MLGoal {Σ : Signature} : Type := mkMLGoal
diff --git a/matching-logic/src/Theories/Bool_Semantics.v b/matching-logic/src/Theories/Bool_Semantics.v
index eb1f448f..109fb872 100644
--- a/matching-logic/src/Theories/Bool_Semantics.v
+++ b/matching-logic/src/Theories/Bool_Semantics.v
@@ -24,8 +24,8 @@ End with_model.
   }.
 
   Instance default_bool_syntax : Bool_Syntax.Syntax := {
-     inj := id;
+     sym_inj := id;
      imported_sorts := 
   }.
 
-End bool_model. *)
\ No newline at end of file
+End bool_model. *)
diff --git a/matching-logic/src/Theories/ProductSort.v b/matching-logic/src/Theories/ProductSort.v
index a8856ba3..c43160c2 100644
--- a/matching-logic/src/Theories/ProductSort.v
+++ b/matching-logic/src/Theories/ProductSort.v
@@ -124,10 +124,10 @@ Section axioms.
         NAAxiom := axiom;
     |}.
     Next Obligation.
-    destruct name; simpl; wf_auto2.
+    destruct name; simpl. all: solve [wf_auto2].
     Qed.
 
     Definition theory := Definedness_Syntax.theory ∪
                        theory_of_NamedAxioms named_axioms.
 
-End axioms.
\ No newline at end of file
+End axioms.
diff --git a/matching-logic/src/Theories/Sorts_Semantics.v b/matching-logic/src/Theories/Sorts_Semantics.v
index a32ed0ae..c46ca12e 100644
--- a/matching-logic/src/Theories/Sorts_Semantics.v
+++ b/matching-logic/src/Theories/Sorts_Semantics.v
@@ -527,7 +527,17 @@ Section with_model.
 
       unfold evar_open. mlSortedSimpl.
       rewrite eval_forall_of_sort_predicate.
-      1: { eauto 8. (* TODO be more explicit. Have a tactic for this kind of goals. *) }
+      1: {
+        match goal with
+        | [ |- M_predicate _ (evar_open _ ?x _) ] => remember x
+        end.
+        unfold evar_open. mlSimpl.
+        case_match; try lia.
+        case_match; try lia.
+        repeat apply M_predicate_impl.
+        all: try apply M_predicate_bott.
+        all: apply (T_predicate_defined _ M M_satisfies_theory).
+      }
       remember
       (fresh_evar
              (! patt_equal
@@ -890,4 +900,3 @@ Hint Resolve M_predicate_exists_of_sort : core.
 
 #[export]
 Hint Resolve M_predicate_forall_of_sort : core.
-
diff --git a/matching-logic/src/Theories/SumSort_Syntax.v b/matching-logic/src/Theories/SumSort_Syntax.v
index fb0fe258..5259ab32 100644
--- a/matching-logic/src/Theories/SumSort_Syntax.v
+++ b/matching-logic/src/Theories/SumSort_Syntax.v
@@ -127,10 +127,10 @@ Open Scope ml_scope.
       NAAxiom := axiom;
     |}.
   Next Obligation.
-    destruct name; simpl; wf_auto2.
+    destruct name; simpl. all: solve [wf_auto2].
   Qed.
 
   Definition theory := Definedness_Syntax.theory ∪
                        theory_of_NamedAxioms named_axioms.
 
-End axioms.
\ No newline at end of file
+End axioms.
diff --git a/matching-logic/src/Utils/stdpp_ext.v b/matching-logic/src/Utils/stdpp_ext.v
index 1ae60858..3f58a8e6 100644
--- a/matching-logic/src/Utils/stdpp_ext.v
+++ b/matching-logic/src/Utils/stdpp_ext.v
@@ -188,7 +188,7 @@ Proof.
 Qed.
 
 (* The same lemma for stdpp's `reverse *)
-Lemma last_reverse_head A (l : list A) (x : A) : option_last (x :: l) = hd_error (reverse l ++ [x]).
+Lemma last_reverse_head A (l : list A) (x : A) : list.last (x :: l) = hd_error (reverse l ++ [x]).
 Proof.
   remember (length l) as len.
   assert (Hlen: length l <= len).
@@ -310,7 +310,7 @@ Proof.
 Abort.
 
 Lemma last_app_singleton {A} (m : A) (l : list A) :
-  option_last (l ++ [m]) = Some m.
+  list.last (l ++ [m]) = Some m.
 Proof.
   induction l.
   - reflexivity.

From 856b5e9e6dcf16935b9188060e76de55eaa51bc0 Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Tue, 28 Jul 2026 06:22:20 +0000
Subject: [PATCH 4/6] Port fixpoint reasoning to Rocq dev

---
 matching-logic/src/FixpointReasoning.v | 84 ++++++--------------------
 matching-logic/src/Utils/stdpp_ext.v   |  2 +-
 2 files changed, 21 insertions(+), 65 deletions(-)

diff --git a/matching-logic/src/FixpointReasoning.v b/matching-logic/src/FixpointReasoning.v
index 6eb4980c..718366d1 100644
--- a/matching-logic/src/FixpointReasoning.v
+++ b/matching-logic/src/FixpointReasoning.v
@@ -221,7 +221,7 @@ Section with_signature.
       Qed.
 
       Definition is_witnessing_sequence_old (m : Domain M) (l : list (Domain M)) :=
-        (last l = Some m) /\
+        (list.last l = Some m) /\
         (match l with
          | [] => False
          | m₀::ms => (m₀ ∈ @eval Σ M ρ base)
@@ -241,7 +241,7 @@ Section with_signature.
       (* This sequence is the reversed version from the informal introduction in line 139 
          For example, for Nat model elements, the witnessing sequence for 5 is [5,4,3,2,1,0] *)
       Definition is_witnessing_sequence (m : Domain M) (l : list (Domain M)) :=
-        (∃ lst, last l = Some lst /\ lst ∈ @eval Σ M ρ base)
+        (∃ lst, list.last l = Some lst /\ lst ∈ @eval Σ M ρ base)
           /\
           hd_error l = Some m
           /\
@@ -421,49 +421,6 @@ Section with_signature.
               (* TODO: would this be easier to use/prove/understand to
                 have `m' ∈ app_ext (eval ρ step) {[m]}` instead? *)
         ) <-> (is_witnessing_sequence m' (m'::l) /\ l ≠ []).
-      Proof.
-        split.
-        - intros [[[lst [Hlst Hbase] ] [Hhd Hwit] ] [step' [Hstep' Hm'] ] ].
-          split.
-          2: { destruct l. simpl in Hhd. inversion Hhd. discriminate. }
-          move: m Hhd m' step' Hm' Hstep'.
-          induction l; intros m Hhd m' step' Hm' Hstep'.
-          + simpl in Hhd. inversion Hhd.
-          + simpl in Hhd. inversion Hhd. subst a. clear Hhd.
-            unfold is_witnessing_sequence.
-            destruct l.
-            { simpl in Hlst. inversion Hlst. subst m. clear Hlst.
-              split.
-              { exists lst. simpl. split. reflexivity. apply Hbase. }
-              simpl. split. reflexivity. apply Forall_cons.
-              split. exists step'. exists lst. split.
-              apply Hstep'. split. constructor. apply Hm'.
-              apply Forall_nil. exact I.
-            }
-            split.
-            { exists lst. split. simpl. simpl in Hlst. apply Hlst. apply Hbase. }
-            split.
-            { reflexivity. }
-            simpl in Hwit. simpl.
-            apply Forall_cons.
-            simpl in IHl. simpl in Hlst.
-            specialize (IHl Hlst).
-            inversion Hwit. subst. clear Hwit.
-            specialize (IHl H2). clear Hlst H2.
-            split.
-            { exists step'. exists m. split. apply Hstep'. split. constructor. apply Hm'. }
-            apply Forall_cons.
-            split.
-            { apply H1. }
-            specialize (IHl d erefl).
-            destruct H1 as [step'' [d'' [Hstep'' [Hd'' Hstep''d''] ] ] ].
-            inversion Hd''. subst d''. clear Hd''.
-            specialize (IHl m step'' Hstep''d'' Hstep'').
-            unfold is_witnessing_sequence in IHl.
-            simpl in IHl.
-            destruct IHl as [_ [_ Hforall] ].
-            inversion Hforall. subst. apply H2.
-        -
       Abort.
 
 
@@ -472,7 +429,7 @@ Section with_signature.
         (is_witnessing_sequence_old m (x::l) /\
         ∃ step', (step' ∈ eval ρ step /\
         m' ∈ app_interp _ step' m)) <->
-        (last (x::l) = Some m /\ is_witnessing_sequence_old m' ((x::l) ++ [m'])).
+        (list.last (x::l) = Some m /\ is_witnessing_sequence_old m' ((x::l) ++ [m'])).
       Proof.
         split.
         -
@@ -487,7 +444,7 @@ Section with_signature.
           { apply Hwit2. }
 
           destruct l.
-          { simpl. apply Forall_cons. split. 2: { apply Forall_nil. exact I. }
+          { simpl. apply Forall_cons. 2: { apply Forall_nil. }
             exists step'. exists x. split.
             { apply Hstep'. }
             split.
@@ -496,19 +453,18 @@ Section with_signature.
           }
           simpl.
           apply Forall_cons.
-          simpl in Hwit3. inversion Hwit3. subst. clear Hwit3.
-          rename H1 into Hd. rename H2 into Hwit.
-          split.
-          { apply Hd. } clear Hd.
+          simpl in Hwit3.
+          { apply (Forall_inv Hwit3). }
 
+          pose proof (Forall_inv_tail Hwit3) as Hwit.
+          clear Hwit3.
           move: d Hwit1 Hwit.
           induction l.
           + intros D Hm _.
             simpl. simpl in Hm. inversion Hm. subst.
             clear Hm.
             apply Forall_cons.
-            split.
-            2: { apply Forall_nil. exact I. }
+            2: { apply Forall_nil. }
             exists step'. exists m. split.
             { apply Hstep'. }
             split.
@@ -517,7 +473,6 @@ Section with_signature.
           + intros d Hlast Hwit. simpl.
             inversion Hwit. subst.
             apply Forall_cons.
-            split.
             { apply H1. }
             apply IHl. simpl in Hlast. simpl. apply Hlast.
             apply H2.
@@ -545,7 +500,7 @@ Section with_signature.
             2: { simpl in Hlen. lia.  }
             simpl. simpl in Hall.
             split.
-            { apply Forall_nil. exact I. }
+            { apply Forall_nil. }
             inversion Hall. subst. clear Hall. clear H2.
             destruct H1 as [step' [m'' [Hstep' [Hm'm'' Hstep'm''] ] ] ].
             inversion Hm'm''. subst. clear Hm'm''.
@@ -560,7 +515,7 @@ Section with_signature.
               clear H2.
               simpl.
               split.
-              { apply Forall_nil. exact I. }
+              { apply Forall_nil. }
               destruct H1 as [step' Hstep'].
               exists step'.
               destruct Hstep' as [m'' [Hstep' [Hmm'' Hm''] ] ].
@@ -571,14 +526,16 @@ Section with_signature.
             }
             simpl in Hall. simpl in IHlen. simpl in Hlast.
             inversion Hall. subst. clear Hall.
-            specialize (IHlen x' l' Hlast H2).
+            assert (Hlen' : length l' <= len) by (simpl in Hlen; lia).
+            specialize (IHlen x' l' Hlast H2 Hlen').
             simpl.
-            rewrite Forall_cons.
-            apply and_assoc.
+            destruct IHlen as [IHfor IHex].
             split.
-            { apply H1. }
-            apply IHlen.
-            simpl in Hlen. lia.
+            { apply Forall_cons.
+              { apply H1. }
+              apply IHfor.
+            }
+            apply IHex.
       Qed.
 
       Definition witnessed_elements_old : propset (Domain M) :=
@@ -720,7 +677,6 @@ Section with_signature.
                 split.
                 { apply Hd. }
                 apply Forall_nil.
-                exact I.
               }
               apply Hm.
             }
@@ -776,7 +732,7 @@ Section with_signature.
             simpl in P.
             rewrite -H2 in P.
 
-            assert (Hm : (match l with [] => Some d1 | _ :: _ => last l end ) = Some mprev).
+            assert (Hm : (match l with [] => Some d1 | _ :: _ => list.last l end ) = Some mprev).
             {
               clear P Heqrev H1 H3 H4 mp.
               destruct l.
diff --git a/matching-logic/src/Utils/stdpp_ext.v b/matching-logic/src/Utils/stdpp_ext.v
index 3f58a8e6..d6e2a860 100644
--- a/matching-logic/src/Utils/stdpp_ext.v
+++ b/matching-logic/src/Utils/stdpp_ext.v
@@ -632,7 +632,7 @@ Proof.
 Qed.
 
 Lemma list_last_length {A : Type} (l : list A):
-  option_last l = l !! (length l - 1).
+  list.last l = l !! (length l - 1).
 Proof.
   remember (length l) as len.
   rewrite Heqlen.

From 75721bad7acff298ec7333401d4d67d4845bfb34 Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Tue, 28 Jul 2026 06:34:20 +0000
Subject: [PATCH 5/6] Keep aborted model experiments compatible with Rocq dev

---
 matching-logic/src/Experimental/Test.v | 43 ++------------------------
 matching-logic/src/Theories/Test.v     | 43 ++------------------------
 2 files changed, 4 insertions(+), 82 deletions(-)

diff --git a/matching-logic/src/Experimental/Test.v b/matching-logic/src/Experimental/Test.v
index 95907f45..d7f633dd 100644
--- a/matching-logic/src/Experimental/Test.v
+++ b/matching-logic/src/Experimental/Test.v
@@ -35,6 +35,7 @@ Require Import
 
 Import MatchingLogic.Logic.Notations.
 Import MatchingLogic.Semantics.Notations.
+Import MatchingLogic.Semantics.
 
 Open Scope ml_scope.
 
@@ -121,50 +122,10 @@ Section natbool.
   Definition get_signature {Σ : Signature} (m : @Model Σ) : Signature := Σ.
 
   Instance def_syntax : @Definedness_Syntax.Syntax (get_signature DefinedNatBoolModel) := {
-    inj _ := inr ();
+    sym_inj _ := inr ();
   }.
 
   Goal DefinedNatBoolModel ⊨ᵀ Definedness_Syntax.theory.
-  Proof.
-    unfold theory, named_axioms, theory_of_NamedAxioms. simpl.
-    unfold satisfies_theory. intros. apply elem_of_PropSet in H.
-    destruct H, x. subst. cbn. unfold satisfies_model. intros.
-    unfold patt_defined, p_x, ev_x. simp eval.
-    unfold app_ext. simpl. unshelve eapply leibniz_equiv.
-    exact (@propset_leibniz_equiv _ DefinedNatBoolModel).
-    eapply set_equiv. intros. split; intros. set_solver.
-    rewrite elem_of_PropSet.
-    exists (inr ()), (evar_valuation ρ (evar_fresh [])).
-    split. set_solver. split. set_solver.
-    case_match. set_solver.
-    (* This condition is unsolvable. It comes from
-     * Mext def -> obligation 1 -> case 4 and
-     * PlainDefinedness def -> app_interp.
-     * These definitions both seen sensible on their own.
-     * Use the second models app_interp if both elements are
-     * from the second model, then wrap it in inr. Also
-     * def $ def is full set (right?). However, when we combine
-     * these, we get something wrong. I suspect this is because
-     * def $ def needs to be full set even AFTER gluing the models,
-     * and not inr <$> full set. We could take as extra params in
-     * ModelCombiners two functions that specifiy these special
-     * behaviours, maybe even functions returning options,
-     * so we retain the default behaviour of delegating to
-     * the sets underlying app_interp. This raises two questions:
-     * - Are there any other cases where this is needed or is this
-     * special to definedness? Should definedness be treated as
-     * special and we don't need this change elsewhere?
-     * ∙ PB: Yes, potentially generic datatypes would raise this issue too.
-       For example, lists, maps, sets. Depending on the element's sort
-       you might need to extend the behaviour of list/set/etc. symbols.
-     * - If we override the models original app_interp, do we not
-     * lose any reasoning we did about the original one? Is there
-     * a way to retain the proofs and allow special behaviour?
-     * ∙ PB: This is a main question. I think, you can only retain the original
-         behaviour, if you override (or rather, extend) the behaviour in a
-         correct way. For example, in case of definedness, you extend its
-         interpretation in M₂ to full.
-     *)
   Abort.
 End natbool.
 
diff --git a/matching-logic/src/Theories/Test.v b/matching-logic/src/Theories/Test.v
index 95907f45..d7f633dd 100644
--- a/matching-logic/src/Theories/Test.v
+++ b/matching-logic/src/Theories/Test.v
@@ -35,6 +35,7 @@ Require Import
 
 Import MatchingLogic.Logic.Notations.
 Import MatchingLogic.Semantics.Notations.
+Import MatchingLogic.Semantics.
 
 Open Scope ml_scope.
 
@@ -121,50 +122,10 @@ Section natbool.
   Definition get_signature {Σ : Signature} (m : @Model Σ) : Signature := Σ.
 
   Instance def_syntax : @Definedness_Syntax.Syntax (get_signature DefinedNatBoolModel) := {
-    inj _ := inr ();
+    sym_inj _ := inr ();
   }.
 
   Goal DefinedNatBoolModel ⊨ᵀ Definedness_Syntax.theory.
-  Proof.
-    unfold theory, named_axioms, theory_of_NamedAxioms. simpl.
-    unfold satisfies_theory. intros. apply elem_of_PropSet in H.
-    destruct H, x. subst. cbn. unfold satisfies_model. intros.
-    unfold patt_defined, p_x, ev_x. simp eval.
-    unfold app_ext. simpl. unshelve eapply leibniz_equiv.
-    exact (@propset_leibniz_equiv _ DefinedNatBoolModel).
-    eapply set_equiv. intros. split; intros. set_solver.
-    rewrite elem_of_PropSet.
-    exists (inr ()), (evar_valuation ρ (evar_fresh [])).
-    split. set_solver. split. set_solver.
-    case_match. set_solver.
-    (* This condition is unsolvable. It comes from
-     * Mext def -> obligation 1 -> case 4 and
-     * PlainDefinedness def -> app_interp.
-     * These definitions both seen sensible on their own.
-     * Use the second models app_interp if both elements are
-     * from the second model, then wrap it in inr. Also
-     * def $ def is full set (right?). However, when we combine
-     * these, we get something wrong. I suspect this is because
-     * def $ def needs to be full set even AFTER gluing the models,
-     * and not inr <$> full set. We could take as extra params in
-     * ModelCombiners two functions that specifiy these special
-     * behaviours, maybe even functions returning options,
-     * so we retain the default behaviour of delegating to
-     * the sets underlying app_interp. This raises two questions:
-     * - Are there any other cases where this is needed or is this
-     * special to definedness? Should definedness be treated as
-     * special and we don't need this change elsewhere?
-     * ∙ PB: Yes, potentially generic datatypes would raise this issue too.
-       For example, lists, maps, sets. Depending on the element's sort
-       you might need to extend the behaviour of list/set/etc. symbols.
-     * - If we override the models original app_interp, do we not
-     * lose any reasoning we did about the original one? Is there
-     * a way to retain the proofs and allow special behaviour?
-     * ∙ PB: This is a main question. I think, you can only retain the original
-         behaviour, if you override (or rather, extend) the behaviour in a
-         correct way. For example, in case of definedness, you extend its
-         interpretation in M₂ to full.
-     *)
   Abort.
 End natbool.
 

From c0089e2dfd1db39dc70015c6d4386ba547a5f55a Mon Sep 17 00:00:00 2001
From: Jason Gross <jason@theorem.dev>
Date: Tue, 28 Jul 2026 07:41:13 +0000
Subject: [PATCH 6/6] Exclude obsolete generated model experiment

---
 matching-logic/src/BasicProofSystemLemmas.v | 26 ++++++++++++---------
 matching-logic/src/dune                     |  3 +++
 2 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/matching-logic/src/BasicProofSystemLemmas.v b/matching-logic/src/BasicProofSystemLemmas.v
index 7f516cca..78470855 100644
--- a/matching-logic/src/BasicProofSystemLemmas.v
+++ b/matching-logic/src/BasicProofSystemLemmas.v
@@ -294,7 +294,7 @@ Proof.
     + exact H3.
     + apply reorder_meta;[wf_auto2|wf_auto2|wf_auto2|].
       apply useBasicReasoning.
-      apply syllogism; wf_auto2.
+      apply syllogism. all: solve [wf_auto2].
 Defined.
 
 Lemma modus_ponens {Σ : Signature} (Γ : Theory) (A B : Pattern) :
@@ -311,7 +311,7 @@ Proof.
       * apply (A_impl_A _ (A ---> B) ltac:(wf_auto2)).
       * eapply (P2 _ (A ---> B) A B ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
     + apply reorder_meta;[wf_auto2|wf_auto2|wf_auto2|].
-      apply syllogism; wf_auto2.
+      apply syllogism. all: solve [wf_auto2].
 Defined.
 
 Lemma not_not_intro {Σ : Signature} (Γ : Theory) (A : Pattern) :
@@ -416,15 +416,17 @@ Proof.
         -- eapply MP.
            ++ exact H0.
            ++ apply useBasicReasoning. 
-              eapply (P1 _ (C ---> D) B _ _).
+              eapply (P1 _ (C ---> D) B
+                ltac:(wf_auto2) ltac:(wf_auto2)).
         -- apply useBasicReasoning.  
-            eapply (P2 _ B C D _ _ _).
+            eapply (P2 _ B C D
+              ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
       * apply useBasicReasoning. 
-        eapply (P1 _ ((B ---> C) ---> B ---> D) A _ _).
+        eapply (P1 _ ((B ---> C) ---> B ---> D) A
+          ltac:(wf_auto2) ltac:(wf_auto2)).
     + apply useBasicReasoning. 
-      eapply (P2 _ A (B ---> C) (B ---> D) _ _ _).
-      Unshelve.
-      all: wf_auto2.
+      eapply (P2 _ A (B ---> C) (B ---> D)
+        ltac:(wf_auto2) ltac:(wf_auto2) ltac:(wf_auto2)).
 Defined.
 
 Lemma bot_elim {Σ : Signature} (Γ : Theory) (A : Pattern) :
@@ -537,9 +539,11 @@ Lemma double_neg_elim {Σ : Signature} (Γ : Theory) (A B : Pattern) :
 Proof.
   intros WFA WFB.
   eapply syllogism_meta.
-  5: apply P4.
-  4: apply P4.
-  all: wf_auto2.
+  - wf_auto2.
+  - wf_auto2.
+  - wf_auto2.
+  - apply P4.
+  - apply P4.
 Defined.
 
 Lemma double_neg_elim_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
diff --git a/matching-logic/src/dune b/matching-logic/src/dune
index 0ddc11a7..6d4eb041 100644
--- a/matching-logic/src/dune
+++ b/matching-logic/src/dune
@@ -1,6 +1,9 @@
 (coq.theory
  (name MatchingLogic)
  (package coq-matching-logic)
+ ; This obsolete, unimported model generator is superseded by
+ ; Theories/DefaultModels.v and does not satisfy the current Bool theory.
+ (modules (:standard \ Experimental.DefaultModelGenerators))
  (synopsis "Matching Logic in Coq")
 )
 (include_subdirs qualified)