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 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3