diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-11 19:08:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-11 21:11:51 +0100 |
| commit | 21abd69648badb999ea22a77cdaad4630761d0e6 (patch) | |
| tree | ad87f0f2680cee0808e9d47b9e146a626bb65615 /pretyping | |
| parent | cc720721075b61a82bc46f43e18b4da6ebbdc8a8 (diff) | |
Accepting conversion on inner closed subterms while looking for
matching subterm destruct/induction on a partially applied
pattern. AFAICS, there is only such instance of destruct that needs
this in the contrins (in EuclideanGeometry/G3_ParticularAngle.v), but
while a more global decision is taken, I prefer at the current time to
adopt this approximation of 8.4 semantics, even if the flags are not
the same when the pattern is fully applied or not. Only so little
cases are concerned because in most cases, destruct/induction on a
partially applied pattern is of the form "destruct cst"
(e.g. "destruct eq_dec") and no conversion is needed anyway.
Not being uniform whether the pattern is fully applied or not is a bit
unsatisfactory, but hopefully, this is temporary.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 982b8a3ec..f52f0f89b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -351,12 +351,15 @@ let default_no_delta_unify_flags () = (* allow_K) because only closed terms are involved in *) (* induction/destruct/case/elim and w_unify_to_subterm_list does not *) (* call w_unify for induction/destruct/case/elim (13/6/2011) *) -let elim_core_flags () = { (default_core_unify_flags ()) with +let elim_core_flags sigma = { (default_core_unify_flags ()) with modulo_betaiota = false; + frozen_evars = + fold_undefined (fun evk _ evars -> Evar.Set.add evk evars) + sigma Evar.Set.empty; } -let elim_flags () = - let flags = elim_core_flags () in { +let elim_flags_evars sigma = + let flags = elim_core_flags sigma in { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = { flags with modulo_delta = empty_transparent_state }; @@ -364,7 +367,9 @@ let elim_flags () = resolve_evars = false } -let elim_no_delta_core_flags () = { (elim_core_flags ()) with +let elim_flags () = elim_flags_evars Evd.empty + +let elim_no_delta_core_flags () = { (elim_core_flags Evd.empty) with modulo_delta = empty_transparent_state; check_applied_meta_types = false; use_pattern_unification = false; @@ -1415,7 +1420,13 @@ let default_matching_flags (sigma,_) = exception PatternNotFound let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = - let flags = default_matching_flags pending in + let flags = + if from_prefix_of_ind then + let flags = default_matching_flags pending in + { flags with core_unify_flags = { flags.core_unify_flags with + modulo_conv_on_closed_terms = Some Names.full_transparent_state; + restrict_conv_on_strict_subterms = true } } + else default_matching_flags pending in let n = List.length (snd (decompose_app c)) in let matching_fun _ t = try |