From 7ac18ed989a884e9d44917c916c7aae016582fe4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 14:23:58 +0200
Subject: Do not export Hints.make_extern.

---
 tactics/hints.mli | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/tactics/hints.mli b/tactics/hints.mli
index ecbde091cd..d8881c3b49 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -225,12 +225,6 @@ val make_resolves :
 val make_resolve_hyp :
   env -> evar_map -> named_declaration -> hint_entry list
 
-(** [make_extern pri pattern tactic_expr] *)
-
-val make_extern :
-  int -> constr_pattern option -> Genarg.glob_generic_argument
-      -> hint_entry
-
 val run_hint : hint ->
   ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
 
-- 
cgit v1.2.3