Tweak reification of proof mode contexts.

theories/vcgen/proofmode.v

@@ -38,7 +38,9 @@ Section tactics.
     - intros. eapply denv_wf_insert; eauto using denv_wf_mono.
       rewrite /dloc_var_wf (prefix_lookup E' _ _ cl) //=.
   Qed.
-  Global Instance prop_into_denv_sep E E' E'' Pin Pin1 Pin2 Pout1 Pout2 Pout m1 m2 m3 :
+  (* Not an instance, due to the IntoSep, this rule will loop if Pin can be
+  split infinitely many times *)
+  Lemma prop_into_denv_sep_aux E E' E'' Pin Pin1 Pin2 Pout1 Pout2 Pout m1 m2 m3 :
     IntoSep Pin Pin1 Pin2 →
     PropIntoDEnv E E' Pin1 Pout1 m1 m2 →
     PropIntoDEnv E' E'' Pin2 Pout2 m2 m3 →
@@ -50,6 +52,19 @@ Section tactics.
     intros. rewrite HP (comm _ Pin1) -assoc HP1 // assoc.
     rewrite (comm _ Pin2) -assoc HP2; last by eauto. by rewrite assoc -HPout.
   Qed.
+  Global Instance prop_into_denv_sep E E' E'' Pin1 Pin2 Pout1 Pout2 Pout m1 m2 m3 :
+    PropIntoDEnv E E' Pin1 Pout1 m1 m2 →
+    PropIntoDEnv E' E'' Pin2 Pout2 m2 m3 →
+    MakeSep Pout1 Pout2 Pout →
+    PropIntoDEnv E E'' (Pin1 ∗ Pin2) Pout m1 m3.
+  Proof. apply prop_into_denv_sep_aux, _. Qed.
+  Global Instance prop_into_denv_mapsto_list E E' E'' q cl vs v vs' Pout1 Pout2 Pout m1 m2 m3 :
+    IsCons vs v vs' →
+    PropIntoDEnv E E' (cl ↦C{q} v) Pout1 m1 m2 →
+    PropIntoDEnv E' E'' ((cl +∗ 1) ↦C{q}∗ vs') Pout2 m2 m3 →
+    MakeSep Pout1 Pout2 Pout →
+    PropIntoDEnv E E'' (cl ↦C{q}∗ vs) Pout m1 m3.
+  Proof. intros ?. apply prop_into_denv_sep_aux, _. Qed.
 
   Global Instance into_denv_nil E : IntoDEnv E E Enil Enil nil.
   Proof. split; unfold denv_interp; eauto. Qed.