From 67da4b45ef65db59b2d7ba1549351d792e1b27d9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:15:37 -0500
Subject: Fix bug #3735: interpretation of "->" in Program follows the standard
 one.

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index 7b50dfae56..f67c34b81b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -397,6 +397,9 @@ Program
 - "Solve Obligations using" changed to "Solve Obligations with",
   consistent with "Proof with".
 - Program Lemma, Definition now respect automatic introduction.
+- Program Lemma, Definition, etc.. now interpret "->" like Lemma and
+  Definition as a non-dependent arrow (potential source of
+  incompatibility).
 - Add/document "Set Hide Obligations" (to hide obligations in the final
   term inside an implicit argument) and "Set Shrink Obligations" (to
   minimize dependencies of obligations defined by tactics).
-- 
cgit v1.2.3