From 783b0af48fc24a2181d960d034d959f265b5d604 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 21 Jul 2014 14:05:35 +0200
Subject: Correct eauto which was not dealing properly with polymorphic
 constants.

---
 tactics/eauto.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0e9d3dcdc8..dbfde64e48 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 = 
-- 
cgit v1.2.3