Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion

is buggy in general.

1 files changed, 10 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
index 751f1e697d..60c9354597 100644
--- a/test-suite/bugs/closed/4394.v
+++ b/test-suite/bugs/closed/4394.v
@@ -1,13 +1,19 @@
 (* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+
 Require Import Equality List.
-Unset Strict Universe Declaration.
-Inductive Foo I A := foo (B : Type) : A -> I B -> Foo I A.
+Inductive Foo (I : Type -> Type) (A : Type) : Type :=
+| foo (B : Type) : A -> I B -> Foo I A.
 Definition Family := Type -> Type.
-Definition fooFamily family : Family := Foo family.
+Definition FooToo : Family -> Family := Foo.
+Definition optionize (I : Type -> Type) (A : Type) := option (I A).
+Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A.
+Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
+Definition barRec : Rec (optionize id) := {| rec := bar id |}.
 Inductive Empty {T} : T -> Prop := .
 Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) :
   Empty (a, b) -> False.
 Proof.
   intro e.
   dependent induction e.
-Qed.
\ No newline at end of file
+Qed.
+