diff options
| author | Pierre-Marie Pédrot | 2015-10-14 12:01:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-14 15:55:06 +0200 |
| commit | 36f669f769fa23eb897adfa0450875a3c0db3476 (patch) | |
| tree | a9ff788fcf6bd5c9cdb3ad8ff4c1b998470fc945 /tactics/hints.mli | |
| parent | 4b8155591be6e20505ee25f7199edcf44a638c7e (diff) | |
Exporting the original unprocessed hint in the hint running function.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index e25b66b27b..af4d3d1f66 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -37,6 +37,7 @@ type 'a hint_ast = | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) type hint +type raw_hint = constr * types * Univ.universe_context_set type hints_path_atom = | PathHints of global_reference list @@ -199,11 +200,11 @@ val make_extern : -> hint_entry val run_hint : hint -> - ((constr * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic + ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic (** This function is for backward compatibility only, not to use in newly written code. *) -val repr_hint : hint -> (constr * clausenv) hint_ast +val repr_hint : hint -> (raw_hint * clausenv) hint_ast val extern_intern_tac : (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t |