aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 00:44:07 +0000