From a25a28e167aabca816a6af37c69a1a72a6be9388 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Apr 2018 17:20:31 +0200
Subject: Files pretyping.ml, glob_obs.ml, evarutil.ml: rewording/typos in some
 comments.

---
 pretyping/glob_ops.mli | 4 ++++
 pretyping/pretyping.ml | 7 ++++---
 2 files changed, 8 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c967f4e884..7bc0140931 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -101,5 +101,9 @@ val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g
 
 val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
+(* [ltac_interp_name subst na] interprets a name according to a name
+   substitution (subst.ltac_idents) and a list of names
+   (subst.ltac_genargs) on which to fail; returns [na] otherwise *)
 val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t
+
 val empty_lvar : Ltac_pretype.ltac_var_map
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a315376aca..42491f4e40 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -417,12 +417,13 @@ let orelse_name name name' = match name with
   | Anonymous -> name'
   | _ -> name
 
+(* Rename identifiers of the (initial part of) typing "rel" env *)
+(* according to a name substitution *)
 let ltac_interp_name_env k0 lvar env sigma =
-  (* envhd is the initial part of the env when pretype was called first *)
-  (* (in practice is is probably 0, but we have to grant the
+  (* ctxt is the initial part of the env when pretype was called first *)
+  (* (in practice k0 is probably 0, but we have to grant the
      specification of pretype which accepts to start with a non empty
      rel_context) *)
-  (* tail is the part of the env enriched by pretyping *)
   let n = Context.Rel.length (rel_context env) - k0 in
   let ctxt,_ = List.chop n (rel_context env) in
   let open Context.Rel.Declaration in
-- 
cgit v1.2.3