From 46a6319c3b96550039a97e169d58825d151cb4d4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 28 Jun 2009 12:18:08 +0000
Subject: Improve return predicate inference by making the return type
 dependent on a matched variable when it is of dependent type, when its type
 allows it (no constructor in the real arguments).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12213 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 23b7661829..436e8e3c39 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1600,19 +1600,22 @@ let prepare_predicate_from_arsign_tycon loc env tomatchs sign arsign c =
 	  | Rel n when dependent tm c 
 		&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
 	      ((n, len) :: subst, len - signlen)
-	  | Rel _ when not (dependent tm c)
-		&& signlen > 1 (* The term is of a dependent type but does not appear in 
-				  the tycon, maybe some variable in its type does. *) ->
+	  | Rel n when signlen > 1 (* The term is of a dependent type,
+				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *)
 		| IsInd (_, IndType(indf,realargs),_) ->
-		    List.fold_left
-		      (fun (subst, len) arg -> 
-			match kind_of_term arg with
+		    let subst = 
+		      if dependent tm c && List.for_all isRel realargs 
+		      then (n, 1) :: subst else subst 
+		    in
+		      List.fold_left
+			(fun (subst, len) arg -> 
+			  match kind_of_term arg with
 			  | Rel n when dependent arg c ->
 			      ((n, len) :: subst, pred len)
 			  | _ -> (subst, pred len))
-		      (subst, len) realargs)
+			(subst, len) realargs)
 	  | _ -> (subst, len - signlen))
       ([], nar) tomatchs arsign
   in
-- 
cgit v1.2.3