diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 13:35:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 13:35:58 +0000 |
| commit | e660d5466bcea7e996a9dce85f37c1280d83097e (patch) | |
| tree | 6e6e4f73d1c7f5df931a16fe3374f589534557f9 /CHANGES | |
| parent | 3b9638f22550c2eaf4da81d7a4aac1633681e565 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5521 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 10 |
1 files changed, 4 insertions, 6 deletions
@@ -8,21 +8,19 @@ Commands if-then-else, notations, projections) - "Functional Scheme" and "Functional Induction" extended to polymorphic types and dependent types - -Syntax - +- Notation now allows recursive patterns, hence recovering parts of V7 Grammar + fonctionalities - Command "Print." discontinued. -- "assert" semantics now consistent with reference manual - Redundant syntax "Implicit Arguments On/Off" discontinued -- Delimiting key %bool for bool_scope added Interpretation scopes -- Add scope %bool +- Delimiting key %bool for bool_scope added - Import no more needed to activate argument scopes from a module Tactics +- "assert" semantics now consistent with reference manual - New tactics stepl and stepr for chaining transitivity steps - Tactic "replace ... with ... in" added |