diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index c9a97bbe..69828715 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: term.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) +(*i $Id: term.mli 15029 2012-03-13 14:47:00Z herbelin $ i*) (*i*) open Names @@ -406,8 +406,7 @@ val it_mkProd_or_LetIn : types -> rel_context -> types (*s 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 |