From 404e5e356d622a871d44b5f778f1fb44ed8555f1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 13 Mar 2012 14:46:55 +0000
Subject: 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
---
 kernel/term.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3