1 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v
new file mode 100644
index 00000000..66343d66
--- /dev/null
+++ b/test-suite/bugs/closed/4251.v
@@ -0,0 +1,17 @@
+
+Inductive array : Type -> Type :=
+| carray : forall A, array A.
+
+Inductive Mtac : Type -> Prop :=
+| bind : forall {A B}, Mtac A -> (A -> Mtac B) -> Mtac B
+| array_make : forall {A}, A -> Mtac (array A).
+
+Definition Ref := array.
+
+Definition ref : forall {A}, A -> Mtac (Ref A) := 
+  fun A x=> array_make x.
+Check array Type.
+Check fun A : Type => Ref A.
+
+Definition abs_val (a : Type) :=
+  bind (ref a) (fun r : array Type => array_make tt).
+\ No newline at end of file