aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
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
2011-06-10Updated CHANGES (info, Show Script, rephrasing).herbelin
2011-06-10Fixing another bug with "_" intro pattern.herbelin
2011-04-28CHANGES updatepboutill
2011-04-28Coqide: try to properly send interrupts to coqtop on Win32letouzey
2011-04-27Updating CHANGESherbelin
2011-04-24Fixed a bug of destruct which was sometimes forgetting local definitions behi...herbelin
2011-04-14Add directories in COQPATH to search path.herbelin
2011-04-08Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395pboutill
2011-04-03Update documentation concerning proofs loading (cf last commit)letouzey
2011-04-01CHANGES: a word about recent changes in coqide, about Ctrl-C in vmletouzey
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
2011-03-17An option "Set Default Timeout n."letouzey
2011-03-07CHANGES: mentionning quickly Separate Extractionletouzey
2011-03-04CHANGES: update of syntax for annotations of functor applicationletouzey
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
2011-02-11Update changelogsglondu
2011-02-10Fixpoints are traverse during implicits arguments search to toplevelpboutill
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 17:56:54 +0000