fix wrong (unsimplified) E in extraction

hferee · Dec 16, 2024 · 8790427 · 8790427
1 parent ffd918c
commit 8790427
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v
@@ -41,8 +41,8 @@ Definition isl_A v f := Af v f.
   Notable exception: (a ∨b) → c *)
 Definition isl_simp f := simp_form f.
 
-Definition isl_simplified_E p ψ := E p [ψ].
-Definition isl_simplified_A p ψ := Af p (ψ).
+Definition isl_simplified_E p ψ := Ef p ψ.
+Definition isl_simplified_A p ψ := Af p ψ.
 
 Set Extraction Output Directory "extraction".