From 471df7db322e77a3cb66a8def53c7ddfdb9c8769 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Nov 2007 10:40:23 +0000
Subject: Suite ajout raccourcis à compute et lazy pour réduire tout sauf
 certaines constantes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10310 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 2d36f32ada..c0fe42112e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,11 @@ Commands
   automatically computed (e.g. Scheme Induction for nat Sort Set).
 - Source of universe inconsistencies now printed when option 
   "Set Printing Universes" is activated,
+- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the "compute" 
+  reduction strategy, respectively meaning reduce only, or everything
+  but, the constants id1 ... idn. "lazy" alone or followed by
+  "[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply
+  all of beta-iota-zeta-delta, possibly restricting delta.
 
 Libraries
 
-- 
cgit v1.2.3