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/1545.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 test-suite/bugs/closed/1545.v (limited to 'test-suite/bugs/closed/1545.v') diff --git a/test-suite/bugs/closed/1545.v b/test-suite/bugs/closed/1545.v new file mode 100644 index 00000000..9ef796fa --- /dev/null +++ b/test-suite/bugs/closed/1545.v @@ -0,0 +1,20 @@ +Module Type TIT. + +Inductive X:Set:= + b:X. +End TIT. + + +Module Type TOTO. +Declare Module t:TIT. +Inductive titi:Set:= + a:t.X->titi. +End TOTO. + + +Module toto (ta:TOTO). +Module ti:=ta.t. + +Definition ex1:forall (c d:ti.X), (ta.a d)=(ta.a c) -> d=c. +intros. +injection H. -- cgit v1.2.3