From 88bc6a84e38ede558386be3eef1d1515af85ea21 Mon Sep 17 00:00:00 2001
From: werner
Date: Tue, 24 Apr 2001 17:30:03 +0000
Subject: interdiction occ positives ET negatives dans Pattern

(en fait dans term.ml, fonction subst_occ_gen
BW


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1698 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index a4adad7626..5d7be75ee4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1598,8 +1598,11 @@ let subst_term_occ_gen locs occ c t =
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
   let check = ref true in
-  let except = List.for_all (fun n -> n<0) locs in
-  let rec substrec (k,c as kc) t =
+  let except = List.exists (fun n -> n<0) locs in
+  if except & (List.exists (fun n -> n>=0) locs) 
+  then error "mixing of positive and negative occurences"
+  else
+   let rec substrec (k,c as kc) t =
     if (not except) & (!pos > maxocc) then t
     else
     if eq_constr t c then
-- 
cgit v1.2.3