aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-17Displaying environment and unfolding aliases in "cannot_unify"herbelin
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
2012-08-23CHANGES: document the end of states/initial.coq and coqtop.optletouzey
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-11Some changes in CHANGES.herbelin
2012-08-08Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.herbelin
2012-08-03Document the command Add/Remove Search Blacklistletouzey
2012-08-03re-sync CHANGES with 8.4letouzey
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-05Quick update to CHANGES, mention especially the new parsing of ->letouzey
2012-06-05CHANGES: mention the end of induction principles for recordsletouzey
2012-05-29Some documentation of recent changes concerning interfacesletouzey
2012-05-23CHANGES: fix a typo + an entry in the wrong sectionletouzey
2012-05-15Intuition: temporary(?) restore the unconditional unfolding of notletouzey
2012-04-17Remove the Dp plugin.gmelquio
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-04-15Update CHANGESherbelin
2012-04-13MSetRBT : implementation of MSets via Red-Black treesletouzey
2012-04-12CHANGES: adapt after backport of some features to 8.4letouzey
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-23Documentation of last commit concerning Backtrackingletouzey
2012-03-19More adaptations of pretyping/coercion to Program mode.msozeau
2012-03-19Fix bugs related to Program integration.msozeau
2012-02-07Documentation for Grab Existential Variables.aspiwack
2012-01-20Breakpoints in Ltac debugger: new command "r foo" to jump to the nextherbelin
2012-01-20Added new command "Set Parsing Explicit" for deactivating parsing (andherbelin
2012-01-19Added the btauto tactic to the documentation.ppedrot
2011-12-26update CHANGES w.r.t. simplgareuselesinge
2011-12-21Cleaning CHANGES file.herbelin
2011-12-19Notifying removal of accidental unfolding of recursive calls ofherbelin
2011-12-17Coq_makefile: if no -install is provided, install location is set by a Makefi...pboutill
2011-12-12CHANGES: some more updatesletouzey
2011-11-29Documentation of appcontextletouzey
2011-11-21Updated CHANGES file wrt to pattern-matching compilation.herbelin
2011-11-20CHANGES updatepboutill
2011-11-20CoqIdE configuration file won't pollute your home anymorepboutill
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-10-22Fixing Equality.injectable which did not detect an equality withoutherbelin
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-23auto with nocore : disable the use of the core database (wish #2188)letouzey
2011-09-16Omega: for non-arithmetical goals, try proving False from context (wish #2236)letouzey
2011-09-12Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...aspiwack
2011-09-01Bug 2577: Second attempt to be correct.pboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 17:44:07 +0000