diff options
| author | Pierre-Marie Pédrot | 2020-06-08 14:23:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | 7ac18ed989a884e9d44917c916c7aae016582fe4 (patch) | |
| tree | 7cc4a08cca26f2c67c324c0f810007de449b205d | |
| parent | f66bd46c551915267a88d1ee2534ba091292882e (diff) | |
Do not export Hints.make_extern.
| -rw-r--r-- | tactics/hints.mli | 6 |
1 files changed, 0 insertions, 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 |