diff options
| -rw-r--r-- | pretyping/unification.ml | 20 | ||||
| -rw-r--r-- | pretyping/unification.mli | 1 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 1 | ||||
| -rw-r--r-- | tactics/auto.ml | 1 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1 | ||||
| -rw-r--r-- | test-suite/success/set.v | 15 |
9 files changed, 41 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5ae824a1b..6f7e2ba6f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -194,11 +194,18 @@ type unify_flags = { (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *) modulo_delta : Names.transparent_state; - (* This controls which constant are unfoldable; this is on for apply *) + (* This controls which constants are unfoldable; this is on for apply *) (* (but not simple apply) since Feb 2008 for 8.2 *) modulo_delta_types : Names.transparent_state; + modulo_delta_in_merge : Names.transparent_state option; + (* This controls whether unfoldability is different when trying to unify *) + (* several instances of the same metavariable *) + (* Typical situation is when we give a pattern to be matched *) + (* syntactically against a subterm but we want the metas of the *) + (* pattern to be modulo convertibility *) + check_applied_meta_types : bool; (* This controls whether meta's applied to arguments have their *) (* type unified with the type of their instance *) @@ -242,6 +249,7 @@ let default_unify_flags = { use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = full_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = true; @@ -254,6 +262,12 @@ let default_unify_flags = { (* in fact useless when not used in w_unify_to_subterm_list *) } +let set_merge_flags flags = + match flags.modulo_delta_in_merge with + | None -> flags + | Some ts -> + { flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts } + (* 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" extends *) @@ -833,7 +847,7 @@ let w_merge env with_types flags (evd,metas,evars) = if Evd.is_defined evd evk then let v = Evd.existential_value evd ev in let (evd,metas',evars'') = - unify_0 curenv evd CONV flags rhs v in + unify_0 curenv evd CONV (set_merge_flags flags) rhs v in w_merge_rec evd (metas'@metas) (evars''@evars') eqns else begin (* This can make rhs' ill-typed if metas are *) @@ -913,7 +927,7 @@ let w_merge env with_types flags (evd,metas,evars) = let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = - unify_0 sp_env evd' CUMUL flags + unify_0 sp_env evd' CUMUL (set_merge_flags flags) (get_type_of sp_env evd' c) ev.evar_concl in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' diff --git a/pretyping/unification.mli b/pretyping/unification.mli index df87283f9..d667ed9a4 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -15,6 +15,7 @@ type unify_flags = { use_metas_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; + modulo_delta_in_merge : Names.transparent_state option; check_applied_meta_types : bool; resolve_evars : bool; use_pattern_unification : bool; diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 2c1b9d21f..18652b767 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -95,6 +95,7 @@ let fail_quick_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = false; resolve_evars = false; use_pattern_unification = false; diff --git a/tactics/auto.ml b/tactics/auto.ml index 7ac79356f..f251b4f85 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1035,6 +1035,7 @@ let auto_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = false; resolve_evars = true; use_pattern_unification = false; diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 8e0dbc6ef..53a284fa8 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -67,6 +67,7 @@ let auto_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = var_full_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = None; check_applied_meta_types = false; resolve_evars = false; use_pattern_unification = true; diff --git a/tactics/equality.ml b/tactics/equality.ml index 1af172bfb..16ee05f9e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -84,6 +84,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = empty_transparent_state; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; @@ -152,6 +153,7 @@ let rewrite_conv_closed_unif_flags = { Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = false; Unification.use_pattern_unification = true; diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 9c27b2951..b2a79dda3 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -285,6 +285,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; @@ -296,11 +297,12 @@ let rewrite_unif_flags = { Unification.allow_K_in_toplevel_higher_order_unification = true } -let rewrite2_unif_flags = +let rewrite2_unif_flags = { Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = conv_transparent_state; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; @@ -318,6 +320,7 @@ let general_rewrite_unif_flags () = Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; Unification.modulo_delta_types = ts; + Unification.modulo_delta_in_merge = None; Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f6f939ed3..abafaa059 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1707,6 +1707,7 @@ let default_matching_flags sigma = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + modulo_delta_in_merge = Some full_transparent_state; check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = false; diff --git a/test-suite/success/set.v b/test-suite/success/set.v index 230192753..8116e8975 100644 --- a/test-suite/success/set.v +++ b/test-suite/success/set.v @@ -1,8 +1,19 @@ +(* This used to fail in 8.0pl1 *) + Goal forall n, n+n=0->0=n+n. intros. - -(* This used to fail in 8.0pl1 *) set n in * |-. +Abort. + +(* This works from 8.4pl1, since merging of different instances of the + same metavariable in a pattern is done modulo conversion *) + +Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1"). + +Goal forall (f:forall n, n=0 -> Prop) n (H:(n+n).+1=0), f (n.+1+n) H. +intros. +set (f _ _). +Abort. |