Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.

Also some dead code.

If no typo is introduced, there should be no semantic changes.

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 9164a4ff26..b16153a39e 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -100,9 +100,9 @@ let check_scheme kind ind = Option.has_some (lookup_scheme kind ind)
 
 let define internal role id c poly univs =
   let id = compute_name internal id in
-  let ctx = UState.minimize univs in
-  let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
-  let univs = UState.univ_entry ~poly ctx in
+  let uctx = UState.minimize univs in
+  let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst uctx) c in
+  let univs = UState.univ_entry ~poly uctx in
   !declare_definition_scheme ~internal ~univs ~role ~name:id c
 
 (* Assumes that dependencies are already defined *)