diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-22 17:55:27 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-22 17:55:27 +0000 |
commit | c32c906ac295e9fe465dbd7b4ce4fc98917fdd7e (patch) | |
tree | 45ff9b071b3e1f5cf8eb2b041eebd6bdc9e00320 /doc | |
parent | 352d52ee7b5b854460361057c642ca1a5e00a7de (diff) |
Amendements apres lecture Bruno
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8441 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rwxr-xr-x | doc/RefMan-pre.tex | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex index 2e53af598..3603c95b2 100755 --- a/doc/RefMan-pre.tex +++ b/doc/RefMan-pre.tex @@ -418,21 +418,16 @@ Secondly, the concrete syntax of terms has been completely revised. The main motivations were \begin{itemize} -\item a more uniform style: all constructions are now lowercase, with a - functional programming perfume (e.g. abstraction is now written {\tt - fun}), and more directly accessible to the novice (e.g. dependent - product is now written {\tt forall}). +\item a more uniform, purified style: all constructions are now lowercase, + with a functional programming perfume (e.g. abstraction is now + written {\tt fun}), and more directly accessible to the novice + (e.g. dependent product is now written {\tt forall} and allows + omission of types). Also, parentheses and are no longer mandatory + for function application. \item extensibility: some standard notations (e.g. ``<'' and ``>'') were incompatible with the previous syntax. Now all standard arithmetic notations (=, +, *, /, <, <=, ... and more) are directly part of the syntax. -\item lighter expressions: the ``(id:t)u'' notation for products - was forbidding the omission of the types. This is now - possible. Also, parentheses are no longer mandatory for function - application. The choice here was to follow the long-standing style of - syntax found in typed functional programming (which is compatible - with polymorphism) rather than the mathematical style (which - harmonizes badly with polymorphism). \end{itemize} Together with the revision of the concrete syntax, a new mechanism of |