From 21abd69648badb999ea22a77cdaad4630761d0e6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 11 Nov 2014 19:08:49 +0100 Subject: 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. --- pretyping/unification.ml | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3