From 359e4ffe307d7d8dd250735373fc6354a58ecff5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Oct 2006 19:35:09 +0000
Subject: Extension du polymorphisme de sorte au cas des définitions dans Type.
 (suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas
 normal qu'on force le type s'il n'est pas déjà présent mais en même temps il
 semble que ce cast serve pour rafraîchir les univers algébriques...)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 61e4ec58e0..5f765c9628 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -291,9 +291,17 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
     | App (f,l) ->
 	let (acc',hdty) =
-	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
-	  then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l)
-	  else mk_hdgoals sigma goal goalacc f
+	  match kind_of_term f with
+	    | Ind ind
+		when not (array_exists occur_meta l) (* we could be finer *) ->
+		(* Sort-polymorphism of inductive types *)
+		goalacc, type_of_inductive_knowing_parameters env sigma ind l
+	    | Const cst
+		when not (array_exists occur_meta l) (* we could be finer *) ->
+		(* Sort-polymorphism of inductive types *)
+		goalacc, type_of_constant_knowing_parameters env sigma cst l
+	    | _ -> 
+		mk_hdgoals sigma goal goalacc f
 	in
 	let (acc'',conclty') =
 	  mk_arggoals sigma goal acc' hdty (Array.to_list l) in
-- 
cgit v1.2.3