Merge branch 'main' into inv

hferee · Sep 11, 2024 · 54b5253 · 54b5253
2 parents d5acbb3 + cae160f
commit 54b5253
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/theories/extraction/UIML_extraction.v b/theories/extraction/UIML_extraction.v
@@ -8,6 +8,7 @@ Require Import KS_export.
 Require Import ISL.PropQuantifiers ISL.DecisionProcedure ISL.Simp.
 
 
+
 Fixpoint MPropF_of_form (f : Formulas.form) : MPropF  :=
 match f with
 | Formulas.Var n => Var n

diff --git a/theories/iSL/DecisionProcedure.v b/theories/iSL/DecisionProcedure.v
@@ -21,7 +21,6 @@ induction l as [|x l].
     * right. simpl. intros z [Hz|Hz]; subst; try rewrite Heq; auto with *.
 Defined.
 
-
 (* This function computes a proof tree of a sequent, if there is one, or produces a proof that there is none *)
 Proposition Proof_tree_dec Γ φ :
   {_ : list_to_set_disj Γ ⊢ φ & True} + {forall H : list_to_set_disj  Γ ⊢ φ, False}.