diff options
Diffstat (limited to 'pretyping/find_subterm.ml')
-rw-r--r-- | pretyping/find_subterm.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index ae8b91c34..df1fc20f1 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -108,7 +108,6 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t = raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in let rec substrec k t = if nowhere_except_in && !pos > maxocc then t else - if not (Vars.closed0 t) then subst_below k t else try let subst = test.match_fun test.testing_state t in if Locusops.is_selected !pos occs then |