From abe0badbe84a90bae4f20541781609ed0ebb3fb9 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Thu, 14 Oct 2021 17:07:25 +0200
Subject: Small optim

---
 src/trace/smtAtom.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 1d608e6..06e1472 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1351,7 +1351,7 @@ module Atom =
                       let c, _ = Structures.decompose_app ty in
                       Structures.eq_constr c (Lazy.force cCompDec)
                  then
-                   (x::[], xs)
+                   ([x], xs)
                  else
                    ([], l)
                | _ -> (x::l1, l2)
-- 
cgit 


From 189b6a17e6dbf2f7f6a396fc81cd384952211091 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Thu, 14 Oct 2021 17:07:50 +0200
Subject: Two examples showing that prenex dependency is handled, but not
 non-prenex one

---
 unit-tests/Tests_verit_tactics.v | 43 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index 2bdc520..2f080a8 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1406,3 +1406,46 @@ Section EqSym.
   Goal hd_error (x :: xs) = Some a /\ tl (x :: xs) = r <-> x :: xs = a :: r.
   Proof. verit. Qed.
 End EqSym.
+
+
+
+Section PrenexDependentTypes.
+  Variables A B : Type.
+  Variable F : Type -> Type.
+  Variable p : B -> F bool.
+  Variable dep : forall (X:Type), A -> F X -> bool.
+  Hypothesis H : forall (x : A) (y : B), dep bool x (p y) = true.
+
+  Hypothesis HF : CompDec (F bool).
+  Hypothesis HA : CompDec A.
+  Hypothesis HB : CompDec B.
+
+  Variable a : A.
+  Variable b : B.
+
+  Goal dep bool a (p b).
+  Proof. verit. Qed.
+
+End PrenexDependentTypes.
+
+
+(*
+Section NonPrenexDependentTypes.
+  Variables A B : Type.
+  Variable F : Type -> Type.
+  Variable p : B -> F bool.
+  Variable dep : A -> forall (X:Type), F X -> bool.
+  Hypothesis H : forall (x : A) (y : B), dep x bool (p y) = true.
+
+  Hypothesis HF : CompDec (F bool).
+  Hypothesis HA : CompDec A.
+  Hypothesis HB : CompDec B.
+
+  Variable a : A.
+  Variable b : B.
+
+  Goal dep a bool (p b).
+  Proof. Fail verit. Qed.
+
+End NonPrenexDependentTypes.
+*)
-- 
cgit