diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-21 14:05:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-21 17:55:55 +0200 |
| commit | 783b0af48fc24a2181d960d034d959f265b5d604 (patch) | |
| tree | fc569c324808393fdd4ba1ae4bc57435f829a268 /tactics | |
| parent | 632eddc87f3ec9fa0511273d005079363183190c (diff) | |
Correct eauto which was not dealing properly with polymorphic constants.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 0e9d3dcdc..dbfde64e4 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -120,8 +120,9 @@ let unify_e_resolve poly flags (c,clenv) gls = let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv else clenv, Univ.empty_level_subst in let clenv' = connect_clenv gls clenv' in - let _ = clenv_unique_resolver ~flags clenv' gls in - Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c) gls + let clenv' = clenv_unique_resolver ~flags clenv' gls in + tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) + (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c)) gls let e_exact poly flags (c,clenv) = let clenv', subst = |