aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-11-22 17:51:32 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-06-14 07:31:22 +0200
commit5e93f1e95853c3614df813845b94051a45f1a749 (patch)
tree06bef8d0dbe5d0d096764a8d70b8c890df2fda31 /pretyping
parent376da97be60957b25e59afb5791fae665127b17b (diff)
Deprecate options that were introduced for compatibility with 8.2.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/unification.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 627a9c9cc..8d87f6e99 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -428,7 +428,7 @@ let automatically_import_coercions = ref false
open Goptions
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "automatic import of coercions";
optkey = ["Automatic";"Coercions";"Import"];
optread = (fun () -> !automatically_import_coercions);
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b4964c1f3..67c8b07e7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -254,7 +254,7 @@ open Goptions
let _ =
declare_bool_option
- { optdepr = false;
+ { optdepr = true; (* remove in 8.8 *)
optname = "pattern-unification for existential variables in tactics";
optkey = ["Tactic";"Pattern";"Unification"];
optread = (fun () -> !global_pattern_unification_flag);