Merge PR #8854: Fix #8364: making univ algebraic when already equal to another.

1 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v
new file mode 100644
index 0000000000..10f955b41f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8364.v
@@ -0,0 +1,17 @@
+Unset Primitive Projections.
+
+Record Box (A:Type) := box { unbox : A }.
+Arguments box {_} _. Arguments unbox {_} _.
+
+Definition map {A B} (f:A -> B) x :=
+  match x with box x => box (f x) end.
+
+Definition tuple (l : Box Type) : Type :=
+  match l with
+  | box x => x
+  end.
+
+Fail Inductive stack : Type -> Type :=
+| Stack T foos :
+  tuple (map stack foos) ->
+  stack T.