diff options
author | 2016-03-09 17:43:12 +0100 | |
---|---|---|
committer | 2016-03-09 17:43:12 +0100 | |
commit | fdbad8894dec9df0294e91aac61ce47d5af609d4 (patch) | |
tree | 9606652bb2c7016c6087c6238a06ed756d460293 /pretyping/unification.ml | |
parent | c633bb322acf0bb626eafe6158287d1ddc11af26 (diff) | |
parent | 2788c86e6a3c089aa7450a7768f8444470e35901 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r-- | pretyping/unification.ml | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 98fd658f2..03a700e17 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -363,6 +363,22 @@ let set_no_delta_flags flags = { resolve_evars = flags.resolve_evars } +(* For the first phase of keyed unification, restrict + to conversion (including beta-iota) only on closed terms *) +let set_no_delta_open_core_flags flags = { flags with + modulo_delta = empty_transparent_state; + modulo_betaiota = false; +} + +let set_no_delta_open_flags flags = { + core_unify_flags = set_no_delta_open_core_flags flags.core_unify_flags; + merge_unify_flags = set_no_delta_open_core_flags flags.merge_unify_flags; + subterm_unify_flags = set_no_delta_open_core_flags flags.subterm_unify_flags; + allow_K_in_toplevel_higher_order_unification = + flags.allow_K_in_toplevel_higher_order_unification; + resolve_evars = flags.resolve_evars +} + (* Default flag for the "simple apply" version of unification of a *) (* type against a type (e.g. apply) *) (* We set only the flags available at the time the new "apply" extended *) @@ -1819,17 +1835,25 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = let allow_K = flags.allow_K_in_toplevel_higher_order_unification in let flags = if occur_meta_or_existential op || !keyed_unification then + (* This is up to delta for subterms w/o metas ... *) flags else (* up to Nov 2014, unification was bypassed on evar/meta-free terms; now it is called in a minimalistic way, at least to possibly unify pre-existing non frozen evars of the goal or of the pattern *) - set_no_delta_flags flags in + set_no_delta_flags flags in + let t' = (strip_outer_cast op,t) in let (evd',cl) = try - (* This is up to delta for subterms w/o metas ... *) - w_unify_to_subterm env evd ~flags (strip_outer_cast op,t) + if is_keyed_unification () then + try (* First try finding a subterm w/o conversion on open terms *) + let flags = set_no_delta_open_flags flags in + w_unify_to_subterm env evd ~flags t' + with e -> + (* If this fails, try with full conversion *) + w_unify_to_subterm env evd ~flags t' + else w_unify_to_subterm env evd ~flags t' with PretypeError (env,_,NoOccurrenceFound _) when allow_K || (* w_unify_to_subterm does not go through evars, so |