diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 14:45:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 16:05:46 +0200 |
| commit | 4cc1714ac9b0944b6203c23af8c46145e7239ad3 (patch) | |
| tree | 5793c3cc93b435c86373855b9bb782f70ae052a6 /tactics/auto.mli | |
| parent | cc42541eeaaec0371940e07efdb009a4ee74e468 (diff) | |
Indexing Proofview.goals with a stage.
This is not perfect though, some primitives are unsound, and some
higher-order API should use polymorphic functions so as not to depend
on a given level.
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index cae180ce7..215544a59 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -26,7 +26,7 @@ val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - [ `NF ] Proofview.Goal.t -> clausenv * constr + ([ `NF ], 'r) Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic |