From 08fa634493b8635a77174bbdcd0e1529e3c40279 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 9 Nov 2015 18:43:50 +0100
Subject: Fix bug #4404: [remember] gives Error: Conversion test raised an
 anomaly.

---
 tactics/tactics.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 37b715ebe..0a013e95f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2345,7 +2345,12 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
-    let t = match ty with Some t -> t | _ -> typ_of env sigma c in
+    let (sigma, t) = match ty with
+    | Some t -> (sigma, t)
+    | None ->
+      let t = typ_of env sigma c in
+      Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t
+    in
     let eq_tac gl = match with_eq with
       | Some (lr,(loc,ido)) ->
           let heq = match ido with
-- 
cgit v1.2.3