From 0b6924f05ef6beb775345f3fb2ad21a009ab3baa Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 29 Mar 2008 11:20:45 +0000
Subject: Fix test-suite files, change conflicting notation "->rel" and the
 others to "-R>" and the like. Split more precisely in inference of case
 predicate between the new code which currently works only for matched
 variables and the old one which works better on variables appearing in
 matched terms types (the two could also be merged).

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

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e1c5beeea2..7c0ed946f5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1586,28 +1586,28 @@ let prepare_predicate_from_arsign_tycon loc env evdref tomatchs sign arsign c =
  * tycon to make the predicate if it is not closed.
  *)
 
+let is_dependent_on_rel x t =
+  match kind_of_term x with
+      Rel n -> not (noccur_with_meta n n t)
+    | _ -> false
+
 let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
   (* No type annotation *)
   | None ->
       (match tycon with
        | Some (None, t) ->
-	   if noccur_with_meta 0 max_int t then
-	     let names,pred =
-	       prepare_predicate_from_tycon loc false env evdref tomatchs sign t
-	     in
-	       Some (build_initial_predicate false names pred)
-	   else
+	   if List.exists (fun (x,_) -> is_dependent_on_rel x t) tomatchs
+	   then
 	     let arsign = extract_arity_signature env tomatchs sign in
 	     let env' = List.fold_right push_rels arsign env in
 	     let names = List.rev (List.map (List.map pi1) arsign) in
 	     let pred = prepare_predicate_from_arsign_tycon loc env' evdref tomatchs sign arsign t in
-	       if eq_constr pred t then
-		 let names,pred =
-		   prepare_predicate_from_tycon loc false env evdref tomatchs sign t
-		 in
-		   Some (build_initial_predicate false names pred)
-	       else
-		 Some (build_initial_predicate true names pred)
+	       Some (build_initial_predicate true names pred)
+	   else
+	     let names,pred =
+	       prepare_predicate_from_tycon loc false env evdref tomatchs sign t
+	     in
+	       Some (build_initial_predicate false names pred)
        | _ -> None)
 
   (* Some type annotation *)
-- 
cgit v1.2.3