From 29d2dcb5474e4eed7e0f0d02d1e388bff53ec82d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 7 Jan 2016 17:21:54 +0100 Subject: Fix a misleading comment for substn_vars --- kernel/vars.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/vars.mli') 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 -- cgit v1.2.3