diff options
| author | Hugo Herbelin | 2018-04-13 17:20:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:27:50 +0200 |
| commit | a25a28e167aabca816a6af37c69a1a72a6be9388 (patch) | |
| tree | 658c83c7d85e3bb23feea666726108f5dccd5a90 | |
| parent | 69fb545f0fad2b356f5be1ce3e1a24b5afe26ce2 (diff) | |
Files pretyping.ml, glob_obs.ml, evarutil.ml: rewording/typos in some comments.
| -rw-r--r-- | engine/evarutil.ml | 4 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 4 | ||||
| -rw-r--r-- | 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 |