aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/unification.ml2
1 files changed, 1 insertions, 1 deletions
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