let-bind result of subsume

theories/lithium/interpreter.v

@@ -463,17 +463,22 @@ Global Hint Extern 1 (CheckOwnInContext ?P) => (liCheckOwnInContext P; construct
 
 (** * Main lithium tactics *)
 Ltac convert_to_i2p_tac P := fail "No convert_to_i2p_tac provided!".
-Ltac convert_to_i2p P cont :=
+Ltac convert_to_i2p P bind cont :=
   lazymatch P with
-  | subsume ?P1 ?P2 ?T => cont uconstr:(((_ : Subsume _ _) _))
-  | subsume_list ?A ?ig ?l1 ?l2 ?f ?T => cont uconstr:(((_ : SubsumeList _ _ _ _ _) _))
+  | subsume ?P1 ?P2 ?T =>
+      bind T ltac:(fun H => uconstr:(subsume P1 P2 H));
+      cont uconstr:(((_ : Subsume _ _) _))
+  | subsume_list ?A ?ig ?l1 ?l2 ?f ?T =>
+      bind T ltac:(fun H => uconstr:(subsume_list A ig l1 l2 f H));
+      cont uconstr:(((_ : SubsumeList _ _ _ _ _) _))
   | _ => let converted := convert_to_i2p_tac P in cont converted
   end.
 Ltac extensible_judgment_hook := idtac.
 Ltac liExtensibleJudgement :=
   lazymatch goal with
-  | |- envs_entails _ ?P =>
-    convert_to_i2p P ltac:(fun converted =>
+  | |- envs_entails ?Δ ?P =>
+      convert_to_i2p P ltac:(fun T tac => li_let_bind T (fun H => let X := tac H in constr:(envs_entails Δ X)))
+                       ltac:(fun converted =>
     simple notypeclasses refine (tac_apply_i2p converted _); [solve [refine _] |]; extensible_judgment_hook
   )end.
 
@@ -761,7 +766,7 @@ Ltac liSideCond :=
 
 Ltac liSep :=
   lazymatch goal with
-  | |- envs_entails _ (bi_sep ?P _) =>
+  | |- envs_entails ?Δ (bi_sep ?P ?Q) =>
     assert_fails (has_evar P);
     lazymatch P with
     | bi_sep _ _ => notypeclasses refine (tac_sep_sep_assoc _ _ _ _ _)
@@ -772,7 +777,9 @@ Ltac liSep :=
     | (□ ?P)%I => notypeclasses refine (tac_do_intro_intuit_sep _ _ _ _ _); [li_pm_reduce|]
     | match ?x with _ => _ end => fail "should not have match in sep"
     | ?P => first [
-               convert_to_i2p P ltac:(fun converted =>
+               convert_to_i2p P
+                 ltac:(fun T tac => li_let_bind T (fun H => let X := tac H in constr:(envs_entails Δ (X ∗ Q))))
+                 ltac:(fun converted =>
                simple notypeclasses refine (tac_apply_i2p_below_sep converted _); [solve[refine _] |])
              | progress liFindHyp FICSyntactic
              | simple notypeclasses refine (tac_fast_apply (tac_do_simplify_goal 0%N _ _) _); [solve [refine _] |]