diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index ee1bfe4d6..1a6521d98 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -614,7 +614,6 @@ let replace_term = replace_term_gen eq_constr 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.exists (fun n -> n<0) locs in if except & (List.exists (fun n -> n>=0) locs) then error "mixing of positive and negative occurences" |