Merge remote-tracking branch 'origin/master' into coq-8.10

2 files changed, 44 insertions, 1 deletions

diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 3e16f6c..9697882 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1351,7 +1351,7 @@ module Atom =
                       let c, _ = CoqInterface.decompose_app ty in
                       CoqInterface.eq_constr c (Lazy.force cCompDec)
                  then
-                   (x::[], xs)
+                   ([x], xs)
                  else
                    ([], l)
                | _ -> (x::l1, l2)
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.
+*)