diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index d5899f1855..a54130efa2 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -435,8 +435,7 @@ val it_mkProd_or_LetIn : types -> rel_context -> types (** {6 Other term destructors. } *) (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair - {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. - It includes also local definitions *) + {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *) val decompose_prod : constr -> (name*constr) list * constr (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair |