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

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3a485e74c..5c0ed9357 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;