From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 28 Oct 2013 14:08:46 +0100
Subject: Initial work on reintroducing old-style polymorphism for
 compatibility (the stdlib does not compile entirely).

---
 proofs/logic.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 02f3a16d8..fb88b8754 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -382,10 +382,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	  match kind_of_term f with
 	    | Ind _ | Const _
 		when (isInd f || has_polymorphic_type (fst (destConst f))) ->
+	      let sigma, ty = 
 		(* Sort-polymorphism of definition and inductive types *)
-		goalacc,
-                type_of_global_reference_knowing_conclusion env sigma f conclty,
-		sigma, f
+		type_of_global_reference_knowing_conclusion env sigma f conclty
+	      in
+		goalacc, ty, sigma, f
 	    | _ ->
 		mk_hdgoals sigma goal goalacc f
 	in
-- 
cgit v1.2.3