diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 1f4c85054d..a3559a693b 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -165,7 +165,10 @@ val prod_applist : Evd.evar_map -> constr -> constr list -> constr (** In [prod_applist_assum n c args], [c] is supposed to have the form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it returns [c] with the assumptions of [Γ] instantiated by [args] and - the local definitions of [Γ] expanded. *) + the local definitions of [Γ] expanded. + Note that [n] counts both let-ins and prods, while the length of [args] + only counts prods. In other words, varying [n] changes how many + trailing let-ins are expanded. *) val prod_applist_assum : Evd.evar_map -> int -> constr -> constr list -> constr (** Remove recursively the casts around a term i.e. |