aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
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
2011-08-18Updates in CHANGESletouzey
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-10Made CHANGES more uniformly writtenherbelin
2011-08-10Less ambitious application of a notation for eq_rect. We proposedherbelin
2011-07-27Typo of bug 2577pboutill
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-07-16Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)herbelin
2011-07-16Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...herbelin
2011-06-19Ensured that the transparency state is used when flag betaiota is on for apply.herbelin
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-18Typo in CHANGESherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 22:44:32 +0000