diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 15:03:10 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-14 13:25:56 +0200 |
| commit | c22ac10752c12bcb23402ad29a73f2d9699248a6 (patch) | |
| tree | 9a77251356af06e08c70f46235815f6a6d4c2bfb /plugins/ltac/evar_tactics.ml | |
| parent | e68f8c904b7ee8fee9f98f75e37ab6d01b54731f (diff) | |
Deprecate Typing.e_* functions
Diffstat (limited to 'plugins/ltac/evar_tactics.ml')
| -rw-r--r-- | plugins/ltac/evar_tactics.ml | 4 |
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 |