From ee6743d2879d874cad13bd05b5be3847ac27062e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 Aug 2014 16:45:10 +0200
Subject: Fixing an unnatural selection of subterms larger than expected in the
 presence of let-ins.

---
 pretyping/unification.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 29ed69b2dd..29d721577f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1526,7 +1526,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
 
 let secondOrderAbstraction env evd flags typ (p, oplist) =
   (* Remove delta when looking for a subterm *)
-  let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
+  let flags = { flags with modulo_delta = empty_transparent_state } in
   let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
   let typp = Typing.meta_type evd' p in
   let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
-- 
cgit v1.2.3