diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-23 19:47:38 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-09 15:24:08 +0200 |
| commit | 1e389def84cc3eafc8aa5d1a1505f078a58234bd (patch) | |
| tree | 7492ba5ed1df0575f8ee4e3dd7894cfe340ff18f /tactics/hints.ml | |
| 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/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 1da464e6f..a1beacd5e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1097,10 +1097,12 @@ exception Found of constr * types let prepare_hint check (poly,local) env init (sigma,c) = let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in - (* We re-abstract over uninstantiated evars. + (* We re-abstract over uninstantiated evars and universes. It is actually a bit stupid to generalize over evars since the first thing make_resolves will do is to re-instantiate the products *) - let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in + let sigma, subst = Evd.nf_univ_variables sigma in + let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in + let c = drop_extra_implicit_args c in let vars = ref (collect_vars c) in let subst = ref [] in let rec find_next_evar c = match kind_of_term c with |