From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/bugs/closed/5323.v | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 test-suite/bugs/closed/5323.v (limited to 'test-suite/bugs/closed/5323.v') diff --git a/test-suite/bugs/closed/5323.v b/test-suite/bugs/closed/5323.v new file mode 100644 index 00000000..295b7cd9 --- /dev/null +++ b/test-suite/bugs/closed/5323.v @@ -0,0 +1,26 @@ +(* Revealed a missing re-consideration of postponed problems *) + +Module A. +Inductive flat_type := Unit | Prod (A B : flat_type). +Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type +-> Type := +| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR. +Inductive op : flat_type -> flat_type -> Type := . +Arguments Op {_ _ _ _} _ _. +Definition bound_op {var} + {src2 dst2} + (opc2 : op src2 dst2) + : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2 + := match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with end. +End A. + +(* A shorter variant *) +Module B. +Inductive exprf (op : unit -> Type) : Type := +| A : exprf op +| Op tR (opc : op tR) (args : exprf op) : exprf op. +Inductive op : unit -> Type := . +Definition bound_op (dst2 : unit) (opc2 : op dst2) + : forall (args2 : exprf op), Op op dst2 opc2 args2 = A op + := match opc2 in op h return (forall args2 : exprf ?[U], Op ?[V] ?[I] opc2 args2 = A op) with end. +End B. -- cgit v1.2.3