diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-01-07 17:21:54 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-01-07 17:23:07 +0100 |
| commit | 29d2dcb5474e4eed7e0f0d02d1e388bff53ec82d (patch) | |
| tree | 38c812891b34872c8cf74c8f2c05e1c6794797c5 /kernel/vars.mli | |
| parent | e309d8119cd82bdf1216751fb076d438782fb60f (diff) | |
Fix a misleading comment for substn_vars
Diffstat (limited to 'kernel/vars.mli')
| -rw-r--r-- | kernel/vars.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli index c0fbeeb6e..9f034b288 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -65,7 +65,7 @@ val subst_var : Id.t -> constr -> constr if two names are identical, the one of least indice is kept *) val subst_vars : Id.t list -> constr -> constr -(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t] +(** [substn_vars n [id1;...;idk] t] substitute [VAR idj] by [Rel j+n-1] in [t] if two names are identical, the one of least indice is kept *) val substn_vars : int -> Id.t list -> constr -> constr |