diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ab962a4cc3..0595a7789a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -65,11 +65,14 @@ let typ_of = Retyping.get_type_of (* Option for 8.2 compatibility *) open Goptions let dependent_propositions_elimination = ref true +let tactic_compat_context = ref false let use_dependent_propositions_elimination () = !dependent_propositions_elimination && Flags.version_strictly_greater Flags.V8_2 +let use_tactic_context_compat () = !tactic_compat_context + let _ = declare_bool_option { optsync = true; @@ -79,6 +82,15 @@ let _ = optread = (fun () -> !dependent_propositions_elimination) ; optwrite = (fun b -> dependent_propositions_elimination := b) } +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "trigger bugged context matching compatibility"; + optkey = ["Tactic";"Compat";"Context"]; + optread = (fun () -> !Flags.tactic_context_compat) ; + optwrite = (fun b -> Flags.tactic_context_compat := b) } + let tactic_infer_flags = { Pretyping.use_typeclasses = true; Pretyping.use_unif_heuristics = true; |