diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-28 06:25:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-09 15:38:49 +0200 |
| commit | 92aea31430f9d0e8a0fc8f0d6b7fd1a221768f6c (patch) | |
| tree | 34ac00f915cc64c87be3e93d3d7c57bb7afea85c /pretyping/find_subterm.ml | |
| parent | 1cdb96f0201b4dda6bdb5f326f60314ae9bf700b (diff) | |
Reverting dbdff037 which does not seem to prevent to have #3638 fixed
on the contrary of message given in 23041481f, while it introduces a
square time complexity of the size of the goal in subterm finding.
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 6733b7fca..1f5435b6b 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -105,7 +105,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 |