diff options
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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; |