diff options
| author | Hugo Herbelin | 2014-08-28 16:45:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-28 17:16:33 +0200 |
| commit | ee6743d2879d874cad13bd05b5be3847ac27062e (patch) | |
| tree | 520640f52b9f9a1e2b594bc2035bad8ad92ef1fb /pretyping | |
| parent | 8b1e0f64e3c2ada90452da301dc5a3a10f4983f8 (diff) | |
Fixing an unnatural selection of subterms larger than expected in the
presence of let-ins.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 2 |
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 |