diff options
| author | herbelin | 2012-03-13 14:46:55 +0000 |
|---|---|---|
| committer | herbelin | 2012-03-13 14:46:55 +0000 |
| commit | 404e5e356d622a871d44b5f778f1fb44ed8555f1 (patch) | |
| tree | e55d4361d788725466aa1948ad970a655e4a7b47 /kernel | |
| parent | 3b8cff45f2a68d4b84374800e1ee021958cccd2a (diff) | |
Fixing vm_compute bug #2729 (function used to decompose constructors
did not handle let-ins and was wrongly specified). Thanks to Pierre
Boutillier and Pierre-Marie Pédrot for pointing out the source of the
bug.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |