aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Unbreak singleton list-like notation (-compat 8.4)Gravatar Jason Gross2016-06-09
* Fix bug #4777: Printing time is impacted by large terms that don't print.Gravatar Pierre-Marie Pédrot2016-06-07
* Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).Gravatar Guillaume Melquiond2016-06-07
* Fixing problems introduced in 8.5 with Ltac trace report. E.g.Gravatar Hugo Herbelin2016-06-06
* Fix incorrect checking of library checksums.Gravatar Maxime Dénès2016-06-05
* Add license text to the windows installationGravatar Enrico Tassi2016-06-03
* Fix proof terminators not being detected in presence of curly brackets (bug #...Gravatar Guillaume Melquiond2016-06-03
* Make "coqdoc -g --parse-comments" behave properly (bug #4773).Gravatar Guillaume Melquiond2016-06-03
* Fix build (use the same mllib file as in trunk).Gravatar Guillaume Melquiond2016-06-02
* Avoid refreshing the segment widget each time a sentence is added.Gravatar Lionel Rieg2016-06-02
* Fix potential race condition in vm_compute.Gravatar Guillaume Melquiond2016-05-31
* Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
* Fix bug #4746: Anomaly: Evar ?X10 was not declared.Gravatar Pierre-Marie Pédrot2016-05-29
* STM: fix argument filtering for slavesGravatar Enrico Tassi2016-05-27
* Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
* rewrite/Univs: Fix bug # 4498.Gravatar Matthieu Sozeau2016-05-26
* Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
* Hints/Univs: fix bug #4628 anomaliesGravatar Matthieu Sozeau2016-05-23
* Disable memoization rather than failing when files cannot be opened.Gravatar Guillaume Melquiond2016-05-20
* native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
* adding "user-contrib" directory to ".gitignore"Gravatar Matej Kosik2016-05-19
* Unicode.ascii_of_ident is now truly injectiveGravatar Pierre Letouzey2016-05-19
* Fix bug #4737: cycle tactic doesn't like zero goals.Gravatar Pierre-Marie Pédrot2016-05-16
* Removing unexcepted activation of option "Regular Subst Tactic", sinceGravatar Hugo Herbelin2016-05-14
* More hints on how to fix compatibility issues.Gravatar Hugo Herbelin2016-05-14
* Small optimization in evar resolution.Gravatar Pierre-Marie Pédrot2016-05-12
* Fix bug #4722: Coq dies when encountering broken symbolic links.Gravatar Pierre-Marie Pédrot2016-05-12
* Fix bug #3887: Better error message for "More than one program with unsolved ...Gravatar Pierre-Marie Pédrot2016-05-09
* Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* Fix typo in configure's option description.Gravatar Guillaume Melquiond2016-05-09
* Use "md5 -q" on FreeBSD architectures (bug #4719).Gravatar Guillaume Melquiond2016-05-09
* Use the actual location of an error in the error pane (bug #4169).Gravatar Guillaume Melquiond2016-05-09
* Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of Module.Gravatar Pierre-Marie Pédrot2016-05-08
* typoGravatar Enrico Tassi2016-05-04
* NPeano : improve compatibility for this deprecated file via compat notationsGravatar Pierre Letouzey2016-05-04
* Int.v: simplify Jason's commit 5b4e3aceGravatar Pierre Letouzey2016-05-04
* Merge branch 'move-compat-notations' of https://github.com/JasonGross/coq int...Gravatar Pierre Letouzey2016-05-04
|\
* | Fixing subst.out after changing spacing in goal output (24a125b77).Gravatar Hugo Herbelin2016-05-04
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:37:49 +0000