aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Extra check at the INSTALL file.Gravatar Hugo Herbelin2015-01-29
* Remove spurious "Loading ML file" and "<W> Grammar extension" from the refere...Gravatar Guillaume Melquiond2015-01-29
* Remove some "Warning:" from the reference manual.Gravatar Guillaume Melquiond2015-01-29
* Prevent spurious warnings about Arguments.Gravatar Guillaume Melquiond2015-01-29
* Made the CoqIDE progress gutter clickable.Gravatar Pierre-Marie Pédrot2015-01-29
* Fix some typos in the documentation.Gravatar Guillaume Melquiond2015-01-29
* Fix some broken Coq scripts in the reference manual.Gravatar Guillaume Melquiond2015-01-29
* Fixing bug #3931.Gravatar Pierre-Marie Pédrot2015-01-28
* Fixed a wrong warning in coq_makefile.Gravatar Pierre Courtieu2015-01-27
* Allow -type-in-type to be an option also for coqc.Gravatar Daniel R. Grayson2015-01-27
* Doc: Overfull lines in chapter on Canonical Structures.Gravatar Hugo Herbelin2015-01-27
* Made replacing of text in CoqIDE atomic w.r.t. the undo/redo.Gravatar Pierre-Marie Pédrot2015-01-25
* Fixing bug #3947.Gravatar Pierre-Marie Pédrot2015-01-25
* Test for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-25
* Doc: Fixing some compilation problems with chapter CanonicalGravatar Hugo Herbelin2015-01-24
* Updating CHANGES (grammar, thanks to AS for pointing it out) +Gravatar Hugo Herbelin2015-01-24
* Removed obsolete option "Legacy Partially Applied EliminationGravatar Hugo Herbelin2015-01-24
* Reference Manual: Documenting new printing of evars and new effect ofGravatar Hugo Herbelin2015-01-24
* Equality Schemes options: reverting commit ff9f94634 which isGravatar Hugo Herbelin2015-01-24
* Isolate a function for printing evar sets.Gravatar Hugo Herbelin2015-01-24
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
* Fix previous commit on extraction.Gravatar Maxime Dénès2015-01-23
* Typos, grammar, layout in CHANGES (continued).Gravatar Hugo Herbelin2015-01-23
* Typos, grammar, layout in CHANGES.Gravatar Hugo Herbelin2015-01-23
* Extraction: fix #3629.Gravatar Maxime Dénès2015-01-23
* Add the possibility of defining opaque terms with program.Gravatar mlasson2015-01-21
* Reference Manual/Credits: expand the paragraph on the new proof engine to mat...Gravatar Arnaud Spiwack2015-01-21
* Reference Manual/Credits: native compute is a major contribution.Gravatar Arnaud Spiwack2015-01-21
* Reference manual/Credits: populate the "various smaller-scale improvements" p...Gravatar Arnaud Spiwack2015-01-21
* Reference Manual/Credits: remove a duplicate.Gravatar Arnaud Spiwack2015-01-21
* Reference manual: pass over the credit section for English.Gravatar Arnaud Spiwack2015-01-21
* Reference manual: fix typo in doc of [tryif/then/else].Gravatar Arnaud Spiwack2015-01-21
* Fix a critical bug in machine arithmetic for native compiler.Gravatar Maxime Dénès2015-01-20
* Making unification of LetIn's expressions more consistent (see #3920).Gravatar Hugo Herbelin2015-01-19
* Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasGravatar Maxime Dénès2015-01-18
* Remove dead code.Gravatar Maxime Dénès2015-01-17
* Fix #3379, now that Require inside modules is allowed again.Gravatar Maxime Dénès2015-01-17
* There was one more universe needed due to the use of now non-universe-polymor...Gravatar Matthieu Sozeau2015-01-18
* Back to 4 expected universes.Gravatar Matthieu Sozeau2015-01-17
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Univs: Complete documentation in refman.Gravatar Matthieu Sozeau2015-01-17
* Partially revert "Forbid Require inside interactive modules and module types."Gravatar Maxime Dénès2015-01-17
* Revert "Adapting two files from test-suite to now forbidden Require's in modu...Gravatar Maxime Dénès2015-01-17
* Revert "Update test for #3363 now that Require is forbidden inside modules."Gravatar Maxime Dénès2015-01-17
* Revert "Fix files in test-suite having to do with Require inside modules."Gravatar Maxime Dénès2015-01-17
* Avoid compilation warning... might not be the best fix though.Gravatar Matthieu Sozeau2015-01-17
* Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-17
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* coq_makefile: install also .v and .globGravatar Enrico Tassi2015-01-16
* Documenting the removal of coercions between sig, sigT, sig2,Gravatar Hugo Herbelin2015-01-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 14:45:52 +0000