diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-14 12:01:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-14 15:55:06 +0200 |
| commit | 36f669f769fa23eb897adfa0450875a3c0db3476 (patch) | |
| tree | a9ff788fcf6bd5c9cdb3ad8ff4c1b998470fc945 /tactics/auto.mli | |
| parent | 4b8155591be6e20505ee25f7199edcf44a638c7e (diff) | |
Exporting the original unprocessed hint in the hint running function.
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 8dacc1362..6e2acf7f5 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -26,9 +26,9 @@ val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags (** Try unification with the precompiled clause, then use registered Apply *) -val unify_resolve_nodelta : polymorphic -> (constr * clausenv) -> unit Proofview.tactic +val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic -val unify_resolve : polymorphic -> Unification.unify_flags -> (constr * clausenv) -> unit Proofview.tactic +val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic (** [ConclPattern concl pat tacast]: if the term concl matches the pattern pat, (in sense of |