aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Traversal of inductive defs in Print AssumptionsGravatar mlasson2015-07-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\
| * Refining 71def2f8 on too strong occur-check limiting evar-evarGravatar Hugo Herbelin2015-07-16
| * Slight improvement in naming anonymous variables in error messages:Gravatar Hugo Herbelin2015-07-16
| * Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Gravatar Hugo Herbelin2015-07-16
| * Remove old test file for #3819 (now fixed).Gravatar Maxime Dénès2015-07-16
| * Fixing bug #4240 (closure_of_filter was not ensuring refinement ofGravatar Hugo Herbelin2015-07-16
| * Test file for #3819.Gravatar Maxime Dénès2015-07-16
| * Fix universe instantiation with canonical structures.Gravatar Maxime Dénès2015-07-16
| * Modules: fix bug #4294Gravatar Matthieu Sozeau2015-07-16
| * Continuing 93579407, spotting other potential sources of anomalyGravatar Hugo Herbelin2015-07-16
| * Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
| * Univs/Inductive: fix typechecking of casesGravatar Matthieu Sozeau2015-07-15
| * STM: fix a "exn with no safe id attached" error on a failing queryGravatar Enrico Tassi2015-07-14
| * Updating checksum in checker (9c732a5cc continued).Gravatar Hugo Herbelin2015-07-12
| * CoqIDE: recenter on backtrack (Close: #4277)Gravatar Enrico Tassi2015-07-11
| * Rewording about how to upgrade on failing calls to constructor.Gravatar Hugo Herbelin2015-07-10
| * Unused variables reported by OCaml.Gravatar Hugo Herbelin2015-07-10
| * Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.Gravatar Hugo Herbelin2015-07-10
| * Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| * Highlighting Universe in CoqIDE.Gravatar Hugo Herbelin2015-07-10
| * CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla.Gravatar Maxime Dénès2015-07-10
| * Native compiler: make non-fatal linking errors silent except in debug mode.Gravatar Maxime Dénès2015-07-10
| * Native compiler: refactor code handling pre-computed values.Gravatar Maxime Dénès2015-07-10
| * Kernel/Checker: Cleanup fixes of substitutions due to let-ins.Gravatar Matthieu Sozeau2015-07-09
| * Kernel: primitive projections handling of let-insGravatar Matthieu Sozeau2015-07-09
| * Improve semantics of -native-compiler flag.Gravatar Maxime Dénès2015-07-09
| * Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
| * Make retyping of projections more resilient to wrong environment.Gravatar Maxime Dénès2015-07-09
| * Fixing printing of primitive coinductive record status.Gravatar Pierre-Marie Pédrot2015-07-09
| * Ide: fix bug #4284 for goodGravatar Matthieu Sozeau2015-07-08
| * Bug 4284: Tentative bugfix for detyping exception.Gravatar Matthieu Sozeau2015-07-08
| * Checker: Report bugfixes from kernel/inductive.mlGravatar Matthieu Sozeau2015-07-08
| * Fix documentation of universes.Gravatar Matthieu Sozeau2015-07-08
| * Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)Gravatar Guillaume Melquiond2015-07-08
| * Fix command-line documentation of coq-tex.Gravatar Guillaume Melquiond2015-07-08
| * Fix documentation.Gravatar Guillaume Melquiond2015-07-08
| * Use the same optimization level for the VM, whatever the debug level.Gravatar Guillaume Melquiond2015-07-08
| * Document Set/Print Firstorder Solver option.Gravatar Matthieu Sozeau2015-07-07
| * Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
| * Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
| * test-suite: Fix test-suite MakefileGravatar Matthieu Sozeau2015-07-07
| * Univs/minimization: Fix unused variable bug.Gravatar Matthieu Sozeau2015-07-07
| * Fixing "Load" without "Verbose" in coqtop, after vernac_com lost itsGravatar Hugo Herbelin2015-07-07
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-06
|\|
* | Temporarily disable test file for #3922.Gravatar Maxime Dénès2015-07-06
| * Test case for #4203, fixed by commit a51cce36.Gravatar Maxime Dénès2015-07-06
| * Fixing documentation (see Maxime's mail on coqdev, July 3).Gravatar Hugo Herbelin2015-07-05
| * More precise rewording about asymmetric patterns.Gravatar Hugo Herbelin2015-07-05
| * Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 06:08:25 +0000