aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
...
* 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
* Updates in CHANGESGravatar letouzey2011-08-18
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
* Made CHANGES more uniformly writtenGravatar herbelin2011-08-10
* Less ambitious application of a notation for eq_rect. We proposedGravatar herbelin2011-08-10
* Typo of bug 2577Gravatar pboutill2011-07-27
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
* This option disables the use of the '{| field := ... |}' notationGravatar herbelin2011-07-16
* Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)Gravatar herbelin2011-07-16
* Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...Gravatar herbelin2011-07-16
* Ensured that the transparency state is used when flag betaiota is on for apply.Gravatar herbelin2011-06-19
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
* Typo in CHANGESGravatar herbelin2011-06-18
* Updated CHANGES (info, Show Script, rephrasing).Gravatar herbelin2011-06-10
* Fixing another bug with "_" intro pattern.Gravatar herbelin2011-06-10
* CHANGES updateGravatar pboutill2011-04-28
* Coqide: try to properly send interrupts to coqtop on Win32Gravatar letouzey2011-04-28
* Updating CHANGESGravatar herbelin2011-04-27
* Fixed a bug of destruct which was sometimes forgetting local definitions behi...Gravatar herbelin2011-04-24
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
* Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395Gravatar pboutill2011-04-08
* Update documentation concerning proofs loading (cf last commit)Gravatar letouzey2011-04-03
* CHANGES: a word about recent changes in coqide, about Ctrl-C in vmGravatar letouzey2011-04-01
* Documentation of the timeout tactical (cf r13917)Gravatar letouzey2011-03-21
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
* CHANGES: mentionning quickly Separate ExtractionGravatar letouzey2011-03-07
* CHANGES: update of syntax for annotations of functor applicationGravatar letouzey2011-03-04
* Extraction: improved indentation of extracted code (fix #2497)Gravatar letouzey2011-03-04
* Update changelogsGravatar glondu2011-02-11
* Fixpoints are traverse during implicits arguments search to toplevelGravatar pboutill2011-02-10
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Update CHANGESGravatar pboutill2011-01-07
* First release of Vector library.Gravatar pboutill2010-12-10
* ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2Gravatar letouzey2010-12-09