diff options
| author | Matthieu Sozeau | 2016-05-23 19:47:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-09 15:24:08 +0200 |
| commit | 1e389def84cc3eafc8aa5d1a1505f078a58234bd (patch) | |
| tree | 7492ba5ed1df0575f8ee4e3dd7894cfe340ff18f /tactics/auto.mli | |
| parent | 1cdb96f0201b4dda6bdb5f326f60314ae9bf700b (diff) | |
Univs/(e)auto: fix bug #4450 polymorphic exact hints
The exact and e_exact tactics were not registering the universes and
constraints of the hint correctly. Now using the same connect_hint_clenv
as unify_resolve, they do. Also correct the implementation of
prepare_hint to normalize the universes of the hint before abstracting
its undefined universes. They are going to be refreshed at each
application. This means that eauto using term can
use multiple different instantiations of the universes of term
if term introduces new universes. If we want just one instantiation
then the term should be abbreviated in the goal first.
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 2e5647f872..0276e8258d 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -26,8 +26,8 @@ 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 - + 'a 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 |