From 404a041fce68b4f7072de0b91b4e136f04250482 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 13:23:05 +0100
Subject: 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.
---
 tactics/ind_tables.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

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 *)
-- 
cgit v1.2.3