Permalink
Browse files

More documentation of new features in CHANGE.

  • Loading branch information...
1 parent c3ce76d commit 816353f8bee87a8ae1c70263cc3f2dc8ad5358cd @ppedrot ppedrot committed May 9, 2014
Showing with 20 additions and 8 deletions.
  1. +20 −8 CHANGES
View
@@ -40,7 +40,8 @@ Vernacular commands
A flag "Set/Unset Record Elimination Schemes" allows to change this.
The tactic "induction" on a record is now actually doing "destruct".
- The "Open Scope" command can now be given also a delimiter (e.g. Z).
-- The "Definition" command now allows the "Local" modifier.
+- The "Definition" command now allows the "Local" modifier, allowing
+ for non-importable definitions.
- The "Let" command can now define local (co)fixpoints.
- Command "Search" has been renamed into "SearchHead". The command
name "Search" now behaves like former "SearchAbout". The latter name
@@ -49,13 +50,8 @@ Vernacular commands
recursively added to the load path, so files from installed libraries
now need to be fully qualified for the "Require" command to find them.
The tools/update-require script can be used to convert a development.
-
-Notations
-
-- The syntax "x -> y" is now declared at level 99. In particular, it has
- now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
- (possible source of incompatibilities)
-- Notations accept term-providing tactics using the $(...)$ syntax.
+- A new Print Strategies command allows to visualize the opacity status
+ of the whole engine.
Specification Language
@@ -68,6 +64,8 @@ Specification Language
Tactics
+- New tactic engine allowing real backtrack and multi-success tactics.
+- New "cbn" tactic, a well-behaved simpl.
- Repeated identical calls to omega should now produce identical proof terms.
- Tactics btauto, a reflexive boolean tautology solver.
- Tactic "tauto" was exceptionally able to destruct other connectives
@@ -122,6 +120,10 @@ Program
Notations
+- The syntax "x -> y" is now declared at level 99. In particular, it has
+ now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
+ (possible source of incompatibilities)
+- Notations accept term-providing tactics using the $(...)$ syntax.
- "Bind Scope" can no longer bind "Funclass" and "Sortclass".
- A notation can be given a (compat "8.x") annotation, making
it behave like a (only parsing), but flags may active warning
@@ -140,6 +142,16 @@ Tools
unchanged.)
- Option -nois prevents coq/theories and coq/plugins to be recursively
added to the load path. (Same behavior as with coq/user-contrib.)
+- coqdep accepts a -dumpgraph option generating a dot file.
+- Makefiles generated through coq_makefile have three new targets "quick"
+ "checkproof" and "vi2vo", allowing respectively to asynchronously compile
+ the files without playing the proof scripts, asynchronously checking
+ that the quickly generated proofs are correct and generating the object
+ files from the quickly generated proofs.
+
+Interfaces
+
+- CoqIDE uses the new STM machinery, allowing for asynchronous edition.
Internal Infrastructure

0 comments on commit 816353f

Please sign in to comment.