From cd20d6508c910f2069864bdde885b63d0d036939 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 21 Nov 2001 23:50:47 +0000
Subject: Quelques autres petits problèmes résolus...

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

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 11c03a23e8..9ea6c85464 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -916,6 +916,26 @@ let infer_predicate loc env isevars typs cstrs ((mis,_) as indf) =
       (true,pred)
 *)
 
+let rec dependent_predicate c = function
+  | PrCcl ccl ->
+      dependent c ccl
+  | PrNotInd (Some t,pred) ->
+      dependent c t or dependent_predicate (lift 1 c) pred
+  | PrNotInd (None,pred) ->
+      dependent_predicate c pred
+  | PrProd (na,NotInd (None,t),pred) ->
+      dependent c t or dependent_predicate (lift 1 c) pred
+  | PrProd (na,NotInd (Some b,t),pred) ->
+      dependent b t or dependent c t or dependent_predicate (lift 1 c) pred
+  | PrProd (na,IsInd (t,_),pred) ->
+      dependent c t or dependent_predicate (lift 1 c) pred
+  | PrLetIn ((args,None),pred) -> 
+      List.exists (dependent c) args or
+      dependent_predicate (lift (List.length args) c) pred
+  | PrLetIn ((args,Some t),pred) ->
+      List.exists (dependent c) args or dependent c t or
+      dependent_predicate (lift (List.length args + 1) c) pred
+
 (* Propagation of user-provided predicate through compilation steps *)
 
 let liftn_predicate n k pred =
@@ -1006,12 +1026,9 @@ let weaken_predicate q pred =
       | PrProd (_,t,pred) ->
 	  (* copt can occur in pred even if the original problem *)
 	  (* is not dependent *)
-	  let dep = 
-            (* We are lazy, and do as if it were always dependent *)
-            true
-            (* dependent_predicate (mkRel 1) pred *)
-          in
+	  let dep = dependent_predicate (mkRel 1) pred in
 	  let copt, p = if dep then Some (mkRel (n+k)), 1 else None, 0 in
+	  let pred = if dep then pred else lift_predicate (-1) pred in
 	  match t with
 	    | IsInd (_,IndType(_,realargs)) ->
 		(* To make it more uniform, we apply realargs but *)
-- 
cgit v1.2.3