| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-12-19 | Fix a typo in Hurkens.v comment | Jason Gross | |
| 2016-12-19 | Bump required OCaml version to 4.02.3. | Maxime Dénès | |
| Was decided during the working group on September, 28th. | |||
| 2016-12-19 | Use Pp.quote in string options. | Maxime Dénès | |
| 2016-12-16 | Fix incorrect documentation that prevents successful compilation (bug #5265). | Guillaume Melquiond | |
| 2016-12-13 | Improve unification debug trace. | Théo Zimmermann | |
| - Add a debug message when applying a heuristic. - Fix double newlines. | |||
| 2016-12-12 | Replace Typeops by Fast_typeops | Gaetan Gilbert | |
| This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial changes in the other files, the real changes are in the parent commit. | |||
| 2016-12-12 | Extend Fast_typeops to be a replacement for Typeops | Gaetan Gilbert | |
| This brings the fix in cad44fc for #2996 to the copy of Fast_typeops.check_hyps_inclusion. Fast_typeops.constant_type checks the universe constraints instead of outputting them. Since everyone who used Typeops.constant_type just discarded the constraints they've been switched to constant_type_in which should be the same in Fast_typeops and Typeops. There are some small differences in the interfaces: - Typeops.type_of_projection <-> Fast_typeops.type_of_projection_constant to avoid collision with the internally used type_of_projection (which gives the type of [Proj(p,c)]). - check_hyps_inclusion takes [('a -> constr)] and ['a] instead of [constr] for reporting errors. | |||
| 2016-12-11 | strengthened the statement of JMeq_eq_dep | Abhishek Anand | |
| because P:U->Prop implies P:U->Type, the new statement is strictly more useful. No change was needed to the proof. | |||
| 2016-12-08 | Set version to 8.6 in configure. | Maxime Dénès | |
| 2016-12-08 | Windows build scripts for 8.6 final. | Maxime Dénès | |
| 2016-12-08 | Fix paths in 32-bit windows build scripts. | Maxime Dénès | |
| 2016-12-07 | Commit bumping the version number was partial... | Maxime Dénès | |
| The sad part of the story is that the script testing this version number is run after tagging by the coq-dev-tools Makefile... will fix that. | |||
| 2016-12-07 | Add bat files for 8.6rc1 build. | Maxime Dénès | |
| 2016-12-07 | Add bat files for 8.6beta1 build. | Maxime Dénès | |
| 2016-12-07 | Set version number to 8.6rc1. | Maxime Dénès | |
| 2016-12-07 | A few words in CHANGES. | Maxime Dénès | |
| 2016-12-07 | ssrmatching: fix iter_constr_LR iterator wrt Proj | Enrico Tassi | |
| 2016-12-07 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-12-06 | Fix #5248 - test-suite fails in 8.6beta1 | Maxime Dénès | |
| This was yet another bug in the VM long multiplication, that I unfortunately introduced in ebc509ed2. It was impacting only 32-bit architectures. In the future, I'll try to make sure that 1) we provide unit tests for integer arithmetic (my int63 branch ships with such tests) 2) our continuous testing infrastructure runs the test suite on a 32-bit architecture. I tried to set up such an instance, but failed. Waiting for support reply. | |||
| 2016-12-06 | Fix broken documentation in presence of \zeroone{... \tt ...}. | Guillaume Melquiond | |
| The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there. | |||
| 2016-12-06 | Update documentation (bugs #5246 and #5251). | Guillaume Melquiond | |
| 2016-12-06 | Merge remote-tracking branch 'github/pr/387' into v8.6 | Maxime Dénès | |
| Was PR#387: ssrmatching: handle primitive projections (fix: #5247) | |||
| 2016-12-06 | Merge remote-tracking branch 'github/pr/389' into v8.6 | Maxime Dénès | |
| Was PR#389: Changed mention of deprecated -byte option to .byte suffix; change module for Coq loop | |||
| 2016-12-05 | Change module for Coq loop | Paul Steckler | |
| 2016-12-05 | the -byte option is deprecated | Paul Steckler | |
| 2016-12-05 | ssrmatching: handle primite projections (fix: #5247) | Enrico Tassi | |
| 2016-12-05 | Compute dependency of C files only in kernel/byterun. | Maxime Dénès | |
| Some C files included in build scripts (in dev/build) were triggering errors or warnings on non-win32 platforms. Note that ide/ide_win32_stubs.c was already handled through an ad-hoc rule in Makefile. If you add a new C file outside of kernel/byterun, please extend the CFILES variable. | |||
| 2016-12-04 | [pp] Set printing width for richpp formatter (bug #5244) | Emilio Jesus Gallego Arias | |
| Richpp output depends on printing width, thus its internal formatter should be seeded with the proper width value. While we are at it, we increase the default buffer size to a more sensible value. | |||
| 2016-12-04 | Merge remote-tracking branch 'github/pr/366' into v8.6 | Maxime Dénès | |
| Was PR#366: Univs: fix bug 5208 | |||
| 2016-12-04 | Merge remote-tracking branch 'github/pr/378' into v8.6 | Maxime Dénès | |
| Was PR#378: Univs: fix bug #5188 | |||
| 2016-12-02 | Fix test-suite after change in "context" printing. | Maxime Dénès | |
| 2016-12-02 | Document changes | Matthieu Sozeau | |
| 2016-12-02 | Merge remote-tracking branch 'github/pr/377' into v8.6 | Maxime Dénès | |
| Was PR#377: Univs: fix bug #5180 | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/372' into v8.6 | Maxime Dénès | |
| Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/368' into v8.6 | Maxime Dénès | |
| Was PR#368: Add example in dev/doc/changes involving Tacmach.project | |||
| 2016-12-02 | Merge branch 'pr/367' into v8.6 | Maxime Dénès | |
| Parts of PR#367: Fixing the "beautifier" and checking the parsing-printing reversibility | |||
| 2016-12-02 | Fixing lexing of strings in comments for beautifier. | Hugo Herbelin | |
| Was a bug introduced in 0ad6edc1. | |||
| 2016-12-02 | Fixing printing of "ltac:" in tactics after surrounding parentheses | Hugo Herbelin | |
| became mandatory. | |||
| 2016-12-02 | Comment on universe handling in Parameters | Matthieu Sozeau | |
| 2016-12-02 | Univs: fix bug #5188 | Matthieu Sozeau | |
| Parameter was implemented the wrong way trying to separate the universes of the telescope. | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/381' into v8.6 | Maxime Dénès | |
| Was PR#381: V8.6+fix typeclasses eauto shelving | |||
| 2016-12-02 | Fix #5242 - Dubious unsilenceable warning on invalid identifier | Maxime Dénès | |
| We make this warning configurable and disabled by default. | |||
| 2016-12-02 | Fixing printing of "Set Warnings Append". | Hugo Herbelin | |
| 2016-12-02 | Fixing space in printing "Context". | Hugo Herbelin | |
| 2016-12-02 | Fixing printers for pr_auto_using and pr_firstorder_using. | Hugo Herbelin | |
| 2016-12-02 | Fixing space in printing several list of implicit arguments. | Hugo Herbelin | |
| 2016-12-02 | Fixing printing of "only parsing" in abbreviations. | Hugo Herbelin | |
| 2016-12-02 | Protect printing of ltac's "context [...]" from possible collision | Hugo Herbelin | |
| with user-level notations by inserting spaces. | |||
| 2016-12-02 | More on fixing #5098 (preserving printing of "in hyp"). | Hugo Herbelin | |
| 2016-12-02 | Merge remote-tracking branch 'github/pr/380' into v8.6 | Maxime Dénès | |
| Was PR#380: Fix bug #5232: proper globalization of hints paths | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |