From c487e02b0b8bffbe3135d7024f25d03a2f5f1af4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 29 Jul 2015 16:37:29 +0200
Subject: Adding test for bug #3779.

---
 test-suite/bugs/closed/3779.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/3779.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v
new file mode 100644
index 0000000000..eb0d206c5c
--- /dev/null
+++ b/test-suite/bugs/closed/3779.v
@@ -0,0 +1,11 @@
+Set Universe Polymorphism.
+Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }.
+Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T.
+Section foo.
+  Universes sm lg.
+  Context (O : UnitSubuniverse@{sm lg}).
+  Context {A : Type@{sm}}.
+  Context (H' : forall (C : Type@{lg}) `{In@{sm lg} O C} (f : A -> C), In@{sm lg} O C).
+  Fail Check (H' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C).
+  Fail Context (H'' : forall (C : Type@{lg}) `{In@{i j} O C} (f : A -> C), In@{j i} O C).
+End foo.
-- 
cgit v1.2.3


From 817308ab59daa40bef09838cfc3d810863de0e46 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 16:53:39 +0200
Subject: Fixing #4221 (interpreting bound variables using ltac env was
 possibly capturing bound names unexpectingly).

We moved renaming to after finding bindings, i.e. in pretyping
"fun x y => x + y" in an ltac environment where y is ltac-bound to x,
we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1"
(which later on is displayed into "fun y y0 => y + y0").

We renounced to renaming in "match" patterns, which was anyway not
working well, as e.g. in

let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0).

which was producing

forall z : nat, match z with 0 => z | S y => y end = 0

because the names in default branches are treated specifically.

It would be easy to support renaming in match again, by putting the
ltac env in the Cases.pattern_matching_problem state and to rename the
names in "typs" (from build_branch), just before returning them at the
end of the function (and similarly in abstract_predicate for the names
occurring in the return predicate).

However, we rename binders in fix which were not interpreted.

There are some difficulties with evar because we want them defined in
the interpreted env (see comment to ltac_interp_name_env).

fix ltac name
---
 test-suite/bugs/closed/4221.v | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/4221.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4221.v b/test-suite/bugs/closed/4221.v
new file mode 100644
index 0000000000..bc120fb1ff
--- /dev/null
+++ b/test-suite/bugs/closed/4221.v
@@ -0,0 +1,9 @@
+(* Some test checking that interpreting binder names using ltac
+   context does not accidentally break the bindings *)
+
+Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False.
+  intros H0 x.
+  lazymatch goal with
+    | [ x : forall k : nat, _ |- _ ]
+      => specialize (fun H0 => x 1 H0)
+  end.
-- 
cgit v1.2.3


From dda6d8f639c912597d5bf9e4f1d8c2c118b8dc48 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 3 Aug 2015 10:31:48 +0200
Subject: Test file for #4254: Mutual inductives with parameters on Type raises
 anomaly.

---
 test-suite/bugs/closed/4254.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/4254.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4254.v b/test-suite/bugs/closed/4254.v
new file mode 100644
index 0000000000..ef219973df
--- /dev/null
+++ b/test-suite/bugs/closed/4254.v
@@ -0,0 +1,13 @@
+Inductive foo (V:Type):Type :=
+  | Foo : list (bar V) -> foo V
+with bar (V:Type): Type :=
+  | bar1: bar V
+  | bar2 : V -> bar V.
+
+Module WithPoly.
+Polymorphic Inductive foo (V:Type):Type :=
+  | Foo : list (bar V) -> foo V
+with bar (V:Type): Type :=
+  | bar1: bar V
+  | bar2 : V -> bar V.
+End WithPoly.
-- 
cgit v1.2.3