diff options
| author | werner | 2001-04-24 17:30:03 +0000 |
|---|---|---|
| committer | werner | 2001-04-24 17:30:03 +0000 |
| commit | 88bc6a84e38ede558386be3eef1d1515af85ea21 (patch) | |
| tree | 901ecbacc282eb809058a84d4c80875d9d8f667a /kernel | |
| parent | 5c0fb1246294ca1a7144af64fa1bdc198c0d24f1 (diff) | |
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
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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 |