aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* Displaying environment and unfolding aliases in "cannot_unify"Gravatar herbelin2013-02-17
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
* CHANGES: document the end of states/initial.coq and coqtop.optGravatar letouzey2012-08-23
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
* Some changes in CHANGES.Gravatar herbelin2012-08-11
* Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.Gravatar herbelin2012-08-08
* Document the command Add/Remove Search BlacklistGravatar letouzey2012-08-03
* re-sync CHANGES with 8.4Gravatar letouzey2012-08-03
* The tactic remember now accepts a final eqn:H option (grant wish #2489)Gravatar letouzey2012-07-09
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Quick update to CHANGES, mention especially the new parsing of ->Gravatar letouzey2012-07-05
* CHANGES: mention the end of induction principles for recordsGravatar letouzey2012-06-05
* Some documentation of recent changes concerning interfacesGravatar letouzey2012-05-29
* CHANGES: fix a typo + an entry in the wrong sectionGravatar letouzey2012-05-23
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
* Remove the Dp plugin.Gravatar gmelquio2012-04-17
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* Update CHANGESGravatar herbelin2012-04-15
* MSetRBT : implementation of MSets via Red-Black treesGravatar letouzey2012-04-13
* CHANGES: adapt after backport of some features to 8.4Gravatar letouzey2012-04-12
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
* Slight change in the semantics of arguments scopes: scopes can noGravatar herbelin2012-03-26
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Documentation of last commit concerning BacktrackingGravatar letouzey2012-03-23
* More adaptations of pretyping/coercion to Program mode.Gravatar msozeau2012-03-19
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Documentation for Grab Existential Variables.Gravatar aspiwack2012-02-07
* Breakpoints in Ltac debugger: new command "r foo" to jump to the nextGravatar herbelin2012-01-20
* Added new command "Set Parsing Explicit" for deactivating parsing (andGravatar herbelin2012-01-20
* Added the btauto tactic to the documentation.Gravatar ppedrot2012-01-19
* update CHANGES w.r.t. simplGravatar gareuselesinge2011-12-26
* Cleaning CHANGES file.Gravatar herbelin2011-12-21
* Notifying removal of accidental unfolding of recursive calls ofGravatar herbelin2011-12-19
* Coq_makefile: if no -install is provided, install location is set by a Makefi...Gravatar pboutill2011-12-17
* CHANGES: some more updatesGravatar letouzey2011-12-12
* Documentation of appcontextGravatar letouzey2011-11-29
* Updated CHANGES file wrt to pattern-matching compilation.Gravatar herbelin2011-11-21
* CHANGES updateGravatar pboutill2011-11-20
* CoqIdE configuration file won't pollute your home anymoreGravatar pboutill2011-11-20
* Add support for XDG_DATA_HOME and XDG_DATA_DIRS.Gravatar pboutill2011-11-20
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
* Fixing Equality.injectable which did not detect an equality withoutGravatar herbelin2011-10-22
* Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedGravatar herbelin2011-10-11
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* auto with nocore : disable the use of the core database (wish #2188)Gravatar letouzey2011-09-23
* Omega: for non-arithmetical goals, try proving False from context (wish #2236)Gravatar letouzey2011-09-16
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* Bug 2577: Second attempt to be correct.Gravatar pboutill2011-09-01