aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-15 22:30:58 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-12-15 22:30:58 +0000
commitc0d273f87a552fa40313df7f4bff0f2deb0c640b (patch)
treee0e2e1aa173e33f2411fe42bba211cb4f2634ecb /CHANGES
parent07dbcbb20f1cccb8bc6e0ef377706c13ff16d631 (diff)
Mise en page
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1131 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES5
1 files changed, 2 insertions, 3 deletions
diff --git a/CHANGES b/CHANGES
index c9dfe0969..cf4398028 100644
--- a/CHANGES
+++ b/CHANGES
@@ -94,9 +94,8 @@ que les 3 primitives), on peut typer avec "constr", "tactic", ou
- Bug affichage Infix corrigé
-- Légère restriction de la syntaxe de Cbv Delta
-
-- L'option [-myconst] de Cbv doit immédiatement suivre Delta
+- Légère restriction de la syntaxe de Cbv Delta : l'option [-myconst]
+ de Cbv doit immédiatement suivre Delta
- End Silent etait interprete comme une fin de section
Begin Silent -> Set Silent