diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-18 21:22:34 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-18 21:22:34 +0200 |
| commit | dbdff037af1a80d223be6e4d093417bae301c583 (patch) | |
| tree | 28f340af14061a81296af854db08d39ff041c7ce /pretyping/find_subterm.ml | |
| parent | a7e66e4f3af85be7a4d345d0f8c6bde5a7a0c7b0 (diff) | |
Do not try to match on a subterm that is not closed in find_subterm.
Diffstat (limited to 'pretyping/find_subterm.ml')
| -rw-r--r-- | pretyping/find_subterm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 61bb2ce03..ef9485487 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -107,6 +107,7 @@ let replace_term_occ_gen_modulo occs 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 |