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.

---
 engine/evarutil.ml     | 4 ++--
 pretyping/glob_ops.mli | 4 ++++
 pretyping/pretyping.ml | 7 ++++---
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b77bf55d8d..b1d880b0ad 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -284,8 +284,8 @@ type csubst = {
   csubst_rev : subst_val Id.Map.t;
   (** Reverse mapping of the substitution *)
 }
-(** This type represent a name substitution for the named and De Bruijn parts of
-    a environment. For efficiency we also store the reverse substitution.
+(** This type represents a name substitution for the named and De Bruijn parts of
+    an environment. For efficiency we also store the reverse substitution.
     Invariant: all identifiers in the codomain of [csubst_var] and [csubst_rel]
     must be pairwise distinct. *)
 
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