From dfe97724fb6034fc06b3ef693f6a3ed94733adbc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Oct 2006 20:11:08 +0000
Subject: Compatibilité du polymorphisme de constantes avec les sections.
 Amélioration affichage des univers. Réparation de petits oublis du premier
 commit. Essai d'une nouvelle stratégie : si le type d'une constante est
 mentionné explicitement, la constante est monomorphe dans Type.

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5f765c9628..33b22c3b73 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -292,14 +292,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | App (f,l) ->
 	let (acc',hdty) =
 	  match kind_of_term f with
-	    | Ind ind
+	    | (Ind _ | Const _)
 		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
+		(* Sort-polymorphism of definition and inductive types *)
+		goalacc, 
+		type_of_global_reference_knowing_parameters env sigma f l
 	    | _ -> 
 		mk_hdgoals sigma goal goalacc f
 	in
@@ -342,8 +339,10 @@ and mk_hdgoals sigma goal goalacc 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)
+	  if isInd f or isConst f 
+	     & not (array_exists occur_meta l) (* we could be finer *)
+	  then
+	    (goalacc,type_of_global_reference_knowing_parameters env sigma f l)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	mk_arggoals sigma goal acc' hdty (Array.to_list l)
-- 
cgit v1.2.3