aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/evar_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/evar_tactics.ml')
-rw-r--r--plugins/ltac/evar_tactics.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 9382f567b..fb6be430f 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -85,9 +85,7 @@ let let_evar name typ =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
- let sigma = ref sigma in
- let _ = Typing.e_sort_of env sigma typ in
- let sigma = !sigma in
+ let sigma, _ = Typing.sort_of env sigma typ in
let id = match name with
| Name.Anonymous ->
let id = Namegen.id_of_name_using_hdchar env sigma typ name in