First attempt at making the distinction between G4IP and G4ISL clear

hferee · Jul 1, 2024 · 583aff1 · 583aff1
1 parent dbfe6f2
commit 583aff1
Show file tree

Hide file tree

Showing 3 changed files with 116 additions and 99 deletions.
diff --git a/theories/iSL/Environments.v b/theories/iSL/Environments.v
@@ -122,7 +122,7 @@ Lemma make_conj_spec x y :
   {x ⊼ y = (x ∧ y)}.
 Proof.
 unfold make_conj.
-repeat (match goal with |- context  [match ?x with | _  => _ end] => destruct x end; try tauto).
+repeat (match goal with |- context  [match ?x with | _  => _ end] => destruct x end; subst; try tauto).
 Qed.
 
 Lemma occurs_in_make_conj v x y : occurs_in v (x ⊼ y) -> occurs_in v x \/ occurs_in v y.