diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/classops.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
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); |