diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 09:47:47 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 09:47:47 +0100 |
| commit | 9122b9244ed0907ce91b50bbe3584d69cb340baa (patch) | |
| tree | 2cdfa907b1e1fb08f48520aa7682d21e6372e539 /pretyping | |
| parent | 7b14d01ccc41b47df9644391bf01e4b7949e571d (diff) | |
| parent | b80f10a95692c3e4fd95f5ed196311e22fc044b4 (diff) | |
Merge PR #6900: [compat] Remove "Tactic Pattern Unification"
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 24 |
1 files changed, 4 insertions, 20 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5bc93f1fa..f4269a2c5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -250,20 +250,6 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -let global_pattern_unification_flag = ref true - -open Goptions - -(* Compatibility option introduced and activated in Coq 8.4 *) - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "pattern-unification for existential variables in tactics"; - optkey = ["Tactic";"Pattern";"Unification"]; - optread = (fun () -> !global_pattern_unification_flag); - optwrite = (:=) global_pattern_unification_flag } - type core_unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; (* What this flag controls was activated with all constants transparent, *) @@ -287,12 +273,10 @@ type core_unify_flags = { use_pattern_unification : bool; (* This solves pattern "?n x1 ... xn = t" when the xi are distinct rels *) - (* This says if pattern unification is tried; can be overwritten with *) - (* option "Set Tactic Pattern Unification" *) + (* This says if pattern unification is tried *) use_meta_bound_pattern_unification : bool; - (* This is implied by use_pattern_unification (though deactivated *) - (* by unsetting Tactic Pattern Unification); has no particular *) + (* This is implied by use_pattern_unification; has no particular *) (* reasons to be set differently than use_pattern_unification *) (* except for compatibility of "auto". *) (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *) @@ -473,10 +457,10 @@ let set_flags_for_type flags = { flags with } let use_evars_pattern_unification flags = - !global_pattern_unification_flag && flags.use_pattern_unification + flags.use_pattern_unification let use_metas_pattern_unification sigma flags nb l = - !global_pattern_unification_flag && flags.use_pattern_unification + flags.use_pattern_unification || flags.use_meta_bound_pattern_unification && Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l |