From 7b4dbbb83e3da2fe716dacad627ddd3497653f07 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Tue, 18 Oct 2016 10:58:42 +0200
Subject: CLEANUP: rename "Nameops.lift_subscript" to
 "Nameops.increment_subscript".

The word "increment" is more appropriate in this case than "lifting".
The world "lifting", in computer science, usually denotes something else:

  https://en.wikipedia.org/wiki/Lambda_lifting
---
 engine/namegen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 1497dbda80..8ab2fdd823 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -170,7 +170,7 @@ let it_mkLambda_or_LetIn_name env b hyps =
 (* Looks for next "good" name by lifting subscript *)
 
 let next_ident_away_from id bad =
-  let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in
+  let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in
   name_rec id
 
 (* Restart subscript from x0 if name starts with xN, or x00 if name
-- 
cgit v1.2.3