From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Apr 2019 13:22:11 +0200
Subject: [api] Remove 8.10 deprecations.

Some of them are significant so presumably it will take a bit of
effort to fix overlays.

I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
---
 vernac/himsg.ml  | 3 ---
 vernac/himsg.mli | 5 -----
 2 files changed, 8 deletions(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f58eeae6dc..b2382ce6fc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1348,9 +1348,6 @@ let explain_pattern_matching_error env sigma = function
   | CannotInferPredicate typs ->
       explain_cannot_infer_predicate env sigma typs
 
-let map_pguard_error = map_pguard_error
-let map_ptype_error = map_ptype_error
-
 let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
       let e = map_ptype_error EConstr.of_constr e in
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index d0f42ea16b..d1c1c092e3 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -43,9 +43,4 @@ val explain_module_error : Modops.module_typing_error -> Pp.t
 val explain_module_internalization_error :
   Modintern.module_internalization_error -> Pp.t
 
-val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
-[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."]
-val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
-[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."]
-
 val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t
-- 
cgit v1.2.3