aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-05-04
* Handle primitive projections inside types when extracting (bug #4616).Gravatar Guillaume Melquiond2016-05-04
* Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.Gravatar Maxime Dénès2016-05-04
* Increase the size of the dumpglob buffer for cooking notations (bug #4708).Gravatar Guillaume Melquiond2016-05-04
* In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* Fix bug #4707: clearbody much slower in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-05-03
* Fix bug #3825: Universe annotations on notations should pass through or be re...Gravatar Pierre-Marie Pédrot2016-05-03
* Test file for #4695: Slow Qed.Gravatar Maxime Dénès2016-05-03
* Fix bug #4292: Unexpected functor objects.Gravatar Pierre-Marie Pédrot2016-05-03
* Use the canonical name when looking for an eliminator (bug #4670).Gravatar Guillaume Melquiond2016-05-03
* Fix bug #4705: coqtop accepts both -emacs and -ideslave.Gravatar Pierre-Marie Pédrot2016-05-03
* Call hooks when terminating a definition proof (bug #4663).Gravatar Guillaume Melquiond2016-05-03
* Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
* Make votour a bit more robust/forgiving with respect to user commands (bug #4...Gravatar Guillaume Melquiond2016-05-02
* Properly handle notations containing spaces (bug #4538).Gravatar Guillaume Melquiond2016-05-02
* Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Gravatar Guillaume Melquiond2016-05-02
* Reduce ide/coq.png to 256x256.Gravatar Guillaume Melquiond2016-04-29
* Fix incorrect cbv reduction of primitive projections. (Bug #4634)Gravatar Guillaume Melquiond2016-04-29
* Make the language grammar much more precise. (Fix bugs #4682 and #4683)Gravatar Guillaume Melquiond2016-04-28
* Update tutorial (fix bug #4699).Gravatar Guillaume Melquiond2016-04-28
* Fix missing newline in coqchk engagement (bug #4694).Gravatar Guillaume Melquiond2016-04-28
* An example for cd139311e, showing a consequence of not convertingGravatar Hugo Herbelin2016-04-28
* Fixing an incompatility introduced in a404360: kernel conversion wasGravatar Hugo Herbelin2016-04-27
* Optimization in building a return clause by pattern-matching: do notGravatar Hugo Herbelin2016-04-27
* Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-04-25
* Print magic numbers in bad magic error messageGravatar Tej Chajed2016-04-25
* One more word about checking 4.01.0 with -debug and camlp4.Gravatar Hugo Herbelin2016-04-24
* Fixing output test Notations2.Gravatar Hugo Herbelin2016-04-22
* Mention problems with fix of #4582 in CHANGES.Gravatar Maxime Dénès2016-04-22
* Mention #4548 (fixed) in CHANGES.Gravatar Maxime Dénès2016-04-22
* Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
* Fixing 50266aab on incompatibility of OCaml 4.01.0 with option -debug.Gravatar Hugo Herbelin2016-04-19
* Revert "Fixing printing of surrounding parentheses in "ltac:"."Gravatar Hugo Herbelin2016-04-19
* Building lazily a few debugging messages involving expressions of commandsGravatar Hugo Herbelin2016-04-17
* Updating configure.ml wrt Coq not compilable with OCaml 4.01.0 in debug mode.Gravatar Hugo Herbelin2016-04-17
* Fixing printing of surrounding parentheses in "ltac:".Gravatar Hugo Herbelin2016-04-17
* Add changelog for 8.5pl1 after the fact.Gravatar Maxime Dénès2016-04-17
* Build stm debugging messages lazily so that they are not silentlyGravatar Hugo Herbelin2016-04-15
* A fix to #4666 (Exc_located capsule added by camlp5 overwritingGravatar Hugo Herbelin2016-04-12
* Quick fix for #4603 (part 2): Anomaly: Universe undefinedGravatar Maxime Dénès2016-04-12
* FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
* TYPOGRAPHY: adding missing \noindent macrosGravatar Matej Kosik2016-04-12
* Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vGravatar Nickolai Zeldovich2016-04-09
* Added compatibility coercions from Specif.v which were present in Coq 8.4.Gravatar Hugo Herbelin2016-04-08
* Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
* Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
* Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-04-07
* Merge PR#152: Add -compat 8.4 econstructor tactics, and testsGravatar Maxime Dénès2016-04-07
|\
* | Use -win32 and -win64 suffixes for installer name on Windows.Gravatar Maxime Dénès2016-04-07
| * Add -compat 8.4 econstructor tactics, and testsGravatar Jason Gross2016-04-05
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 10:48:01 +0000