From dbdff037af1a80d223be6e4d093417bae301c583 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 18 Sep 2014 21:22:34 +0200
Subject: Do not try to match on a subterm that is not closed in find_subterm.

---
 pretyping/find_subterm.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/find_subterm.ml')

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
-- 
cgit v1.2.3