diff options
| author | mohring | 2003-01-17 15:11:24 +0000 |
|---|---|---|
| committer | mohring | 2003-01-17 15:11:24 +0000 |
| commit | fba8e67f0cec873727ad4612cfc8adf674582dba (patch) | |
| tree | a7ea0dffde18852e15463f21d39316b4a8672146 | |
| parent | 8fd1080fcfd0b7f3f462cd0ccea03632c8e1dc21 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3520 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -1,8 +1,6 @@ -Changes from V7.3.1 to ???? +Changes from V7.3.1 to V7.4 ------------------------- -TODO: unification 2eme ordre avec NewDestruct - Grammar extension - In old syntax, the only predefined non-terminal entries are ident, @@ -39,6 +37,7 @@ Library Language +- Modules (see doc chap 2.5 for commands and chap 4 for theory) - Inductive definitions now accept ">" in constructor types to declare the corresponding constructor as a coercion. - Idem for assumptions declarations and constants when the type is mentionned. @@ -65,6 +64,7 @@ ML tactic and vernacular commands COMMAND EXTEND. - "Check n c" now "n:Check c", "Eval n ..." now "n:Eval ..." - "Proof with T" (* no documentation *) + Tactic definitions - static globalisation of identifiers and global references (source of |