From 5b7b0e5d1ccbc86598370c03f1bbb6543bb92570 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 11 Apr 2006 07:05:50 +0000
Subject: patch pour contourner l'échec de type_of_applied_inductive sur un
 inductif appliqué à des meta non castés (à défaut de comprendre comment gérer
 le flux de typage des metas : besoin du type de l'inductive pour caster les
 metas arguments directs mais besoin de caster les metas arguments directs
 pour connaitre le type d'un inductif à polymorphisme de sorte)

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

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 36409794c5..bbc1e202c0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -284,7 +284,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
     | App (f,l) ->
 	let (acc',hdty) =
-	  if isInd f 
+	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
 	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
 	  else mk_hdgoals sigma goal goalacc f
 	in
@@ -326,7 +326,7 @@ and mk_hdgoals sigma goal goalacc trm =
 
     | App (f,l) ->
 	let (acc',hdty) = 
-	  if isInd f 
+	  if isInd f & not (array_exists occur_meta l) (* we could be finer *)
 	  then (goalacc,type_of_applied_inductive env sigma (destInd f) l)
 	  else mk_hdgoals sigma goal goalacc f
 	in
-- 
cgit v1.2.3