From b30ca8ac9e0225e6505fea0004ea37e7649c9cb6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Nov 2015 17:25:49 -0500
Subject: Fix bug in proofs/logic.ml
 type_of_global_reference_knowing_conclusion is buggy in general.

---
 proofs/logic.ml               |  6 ++++--
 tactics/tactics.ml            |  2 +-
 test-suite/bugs/closed/4394.v | 14 ++++++++++----
 3 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5c48995fc7..3273c95728 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -356,9 +356,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
 	  if is_template_polymorphic env f then
-	    let sigma, ty = 
+	    let ty = 
 	      (* Template sort-polymorphism of definition and inductive types *)
-	      type_of_global_reference_knowing_conclusion env sigma f conclty
+	      let firstmeta = Array.findi (fun i x -> occur_meta x) l in
+	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
+	        type_of_global_reference_knowing_parameters env sigma f args
 	    in
 	      goalacc, ty, sigma, f
 	  else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7756553e2d..2a46efd8ef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3329,7 +3329,7 @@ let abstract_args gl generalize_vars dep id defined f args =
 	if defined then Some c', typ_of ctxenv !sigma c'
 	else None, c'
       in
-      let term = make_abstract_generalize gl id concl dep ctx body c' eqs args refls in
+      let term = make_abstract_generalize {gl with sigma = !sigma} id concl dep ctx body c' eqs args refls in
 	Some (term, !sigma, dep, succ (List.length ctx), vars)
     else None
 
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.
+
-- 
cgit v1.2.3