index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
CHANGES
Commit message (
Expand
)
Author
Age
*
Quick update to CHANGES, mention especially the new parsing of ->
letouzey
2012-07-05
*
CHANGES: mention the end of induction principles for records
letouzey
2012-06-05
*
Some documentation of recent changes concerning interfaces
letouzey
2012-05-29
*
CHANGES: fix a typo + an entry in the wrong section
letouzey
2012-05-23
*
Intuition: temporary(?) restore the unconditional unfolding of not
letouzey
2012-05-15
*
Remove the Dp plugin.
gmelquio
2012-04-17
*
Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).
herbelin
2012-04-15
*
Update CHANGES
herbelin
2012-04-15
*
MSetRBT : implementation of MSets via Red-Black trees
letouzey
2012-04-13
*
CHANGES: adapt after backport of some features to 8.4
letouzey
2012-04-12
*
info_trivial, info_auto, info_eauto, and debug (trivial|auto)
letouzey
2012-03-30
*
Slight change in the semantics of arguments scopes: scopes can no
herbelin
2012-03-26
*
Module names and constant/inductive names are now in two separate namespaces
letouzey
2012-03-26
*
Documentation of last commit concerning Backtracking
letouzey
2012-03-23
*
More adaptations of pretyping/coercion to Program mode.
msozeau
2012-03-19
*
Fix bugs related to Program integration.
msozeau
2012-03-19
*
Documentation for Grab Existential Variables.
aspiwack
2012-02-07
*
Breakpoints in Ltac debugger: new command "r foo" to jump to the next
herbelin
2012-01-20
*
Added new command "Set Parsing Explicit" for deactivating parsing (and
herbelin
2012-01-20
*
Added the btauto tactic to the documentation.
ppedrot
2012-01-19
*
update CHANGES w.r.t. simpl
gareuselesinge
2011-12-26
*
Cleaning CHANGES file.
herbelin
2011-12-21
*
Notifying removal of accidental unfolding of recursive calls of
herbelin
2011-12-19
*
Coq_makefile: if no -install is provided, install location is set by a Makefi...
pboutill
2011-12-17
*
CHANGES: some more updates
letouzey
2011-12-12
*
Documentation of appcontext
letouzey
2011-11-29
*
Updated CHANGES file wrt to pattern-matching compilation.
herbelin
2011-11-21
*
CHANGES update
pboutill
2011-11-20
*
CoqIdE configuration file won't pollute your home anymore
pboutill
2011-11-20
*
Add support for XDG_DATA_HOME and XDG_DATA_DIRS.
pboutill
2011-11-20
*
Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructors
letouzey
2011-11-07
*
Fixing Equality.injectable which did not detect an equality without
herbelin
2011-10-22
*
Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed
herbelin
2011-10-11
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
auto with nocore : disable the use of the core database (wish #2188)
letouzey
2011-09-23
*
Omega: for non-arithmetical goals, try proving False from context (wish #2236)
letouzey
2011-09-16
*
Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...
aspiwack
2011-09-12
*
Bug 2577: Second attempt to be correct.
pboutill
2011-09-01
*
Updates in CHANGES
letouzey
2011-08-18
*
Propagated information from the reduction tactics to the kernel so
herbelin
2011-08-10
*
Made CHANGES more uniformly written
herbelin
2011-08-10
*
Less ambitious application of a notation for eq_rect. We proposed
herbelin
2011-08-10
*
Typo of bug 2577
pboutill
2011-07-27
*
This adds two option tables 'Printing Record' and 'Printing Constructor'
herbelin
2011-07-16
*
This option disables the use of the '{| field := ... |}' notation
herbelin
2011-07-16
*
Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)
herbelin
2011-07-16
*
Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...
herbelin
2011-07-16
*
Ensured that the transparency state is used when flag betaiota is on for apply.
herbelin
2011-06-19
*
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
*
Generalizing flag use_evars_pattern_unification into a flag
herbelin
2011-06-18
[next]