From 6d881b85ee86ca05f8c9e50f060242eb6cf0455d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 2 Dec 2002 19:02:23 +0000
Subject: Ajout des options "Set Contextual Implicits" et "Set Strict Implicits

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

diff --git a/CHANGES b/CHANGES
index e3393dc6e1..238976a72b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -87,6 +87,16 @@ Miscellaneous
 
 - Printing Coercion now used through the standard keywords Set/Add, Test, Print
 - "Print Term id" is an alias for "Print id"
+- New switch "Unset/Set Printing Symbols" to control printing of
+  symbolic notations
+- Two new variants of implicit arguments are available
+   - "Unset/Set Contextual Implicits" tells to consider implicit also the
+     arguments inferable from the context (e.g. for nil or refl_eq)
+   - "Unset/Set Strict Implicits" tells to consider implicit only the
+     arguments that are inferable in any case (i.e. arguments that occurs
+     as argument of rigid constants in the type of the remaining arguments;
+     e.g. the witness of an existential is not strict since it can vanish when
+     applied to a predicate which does not use its argument)
 
 Incompatibilities
 
-- 
cgit v1.2.3