diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 3 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 8 |
2 files changed, 7 insertions, 4 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index e7b2a0e8a6..71155d7921 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -896,7 +896,8 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in + let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in + (** FIXME: provide a proper naming for the bound variables *) quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 13c8830b84..9cbaa8af9b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -114,8 +114,8 @@ type hint_mode = Hints.hint_mode = [@@ocaml.deprecated "Please use [Hints.hint_mode]"] type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = - { hint_priority : int option; - hint_pattern : 'a option } + { hint_priority : int option; [@ocaml.deprecated "Use Typeclasses.hint_priority"] + hint_pattern : 'a option [@ocaml.deprecated "Use Typeclasses.hint_pattern"] } [@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] type hint_info_expr = Hints.hint_info_expr @@ -151,7 +151,9 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) -type opacity_flag = Proof_global.opacity_flag = Opaque | Transparent +type opacity_flag = Proof_global.opacity_flag = + Opaque [@ocaml.deprecated "Use Proof_global.Opaque"] + | Transparent [@ocaml.deprecated "Use Proof_global.Transparent"] [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"] type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option |