From dd669a4b77452690abb3e52c8e66f6510885374b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 19 Mar 2005 11:25:19 +0000
Subject: Le type d'un Let est considéré comme 'user-provided' par le noyau et
 doit donc avoir des univers frais

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6862 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3a485e74cb..5c0ed93575 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -738,7 +738,7 @@ let letin_tac with_eq name c occs gl =
       if not (mem_named_context x (pf_hyps gl)) then x else
 	error ("The variable "^(string_of_id x)^" is already declared") in
   let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in 
-  let t = pf_type_of gl c in
+  let t = refresh_universes (pf_type_of gl c) in
   let newcl = mkNamedLetIn id c t ccl in
   tclTHENLIST
     [ convert_concl_no_check newcl;
-- 
cgit v1.2.3