| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| | | | | | | * | | | | | | | | | | | Fix TypeclassDebug.out after conflicting PR merges |  Matthieu Sozeau | 2017-07-26 | |
| | |_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | test-suite/success/extraction.v : add some Extraction TestCompile |  Pierre Letouzey | 2017-07-26 | |
| | | | | | | | | | | | | | | * | | Enrich test file 4720.v with a compilation test of the extracted code | Pierre Letouzey | 2017-07-26 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | adding a test-suite file 4709.v (thanks to the new command Extraction TestCom... | Pierre Letouzey | 2017-07-26 | |
| | | | | | | | | | | * | | | | | Extraction: reduce primitive projections in types (fix bug 4709) | Pierre Letouzey | 2017-07-26 | |
| | |_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | Remove a few useless evar-normalizations in printing code. |  Pierre-Marie Pédrot | 2017-07-26 | |
| | |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | Add a comment regarding the specialization of the combinator in Detyping. | Pierre-Marie Pédrot | 2017-07-26 | |
| * | | | | | | | | | | | | | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844... |  Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #910: Add [opam update] and online repository to gitlab CI script. | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | * | | | | Removing default evar-normalization for ARGUMENT EXTEND. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | | | |/ / / / | | | | | | | | | |/| | | | | ||||
| * | | | | | | | | | | | | | | Merge PR #886: Fixing what was presumably a typo in the naming conventions file | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #902: Only perform profile initialization and printing when the flag... | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | | Removing template polymorphism for definitions. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | |/ / / / / / / | ||||
| * | | | | | | | | | | | | | | | Merge PR #894: Fixing a little location bug with recursive binders | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #882: Adding a V8.7 compatibility version number. | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | * | | | | | | | Avoiding a variable shadowing in the kernel. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | | | * | | | | | | | Statically ensuring that inlined entries out of the kernel have no effects. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | | | * | | | | | | | Further simplication: do not recreate entries for side-effects. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | | | * | | | | | | | Remove a horrendous hack in Declare to retrieve exported side-effects. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | | | * | | | | | | | More precise type of entries capturing their lack of side-effects. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | | | * | | | | | | | Using a record type for Cooking.result. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | | | * | | | | | | | More precise type for universe entries. | Pierre-Marie Pédrot | 2017-07-26 | |
| | | | | | | | | | | | |/ / / / / | | | | | | | | | | |/| | | | | | ||||
| * | | | | | | | | | | | | | | | | Merge PR #885: Removing a dummy parameter in some FMapPositive statements. | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | * | | | | Adding support for recursive notations of the form "x , .. , y , z". |  Hugo Herbelin | 2017-07-26 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | Merge PR #868: Fix debug trace of typeclasses eauto. | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #845: Add Z.mod_div lemma to standard library. | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | Merge PR #905: [api] Remove type equalities from API. | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #857: Extraction: various fixes related with bug 4720 | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #859: Extraction TestCompile | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #808: [api] Put some order in API.mli | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #750: Remove deprecated options of ./configure in 8.8 | Maxime Dénès | 2017-07-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | * | | | | | | | | | | | | | | | | | make sure that API-leaks cannot be reintroduced by mistake |  Matej Košík | 2017-07-26 | |
| * | | | | | | | | | | | | | | | | | | | | | | Makefile.ide: restore a coqide-binaries rule (fix bug 5667) | Pierre Letouzey | 2017-07-25 | |
| | | | | | * | | | | | | | | | | | | | | | | | [api] Remove type equalities from API. |  Emilio Jesus Gallego Arias | 2017-07-25 | |
| | | | |_|/ / / / / / / / / / / / / / / / / | | |/| | | | | | | | | | | | | | | | | | | ||||
| | | * | | | | | | | | | | | | | | | | | | | [api] Put modules in order in API.{mli,ml} | Emilio Jesus Gallego Arias | 2017-07-25 | |
| | |/ / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | * | | Adding -print-version in addition to -print-version for consistency. | Hugo Herbelin | 2017-07-25 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | | | | | Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484... | Pierre Letouzey | 2017-07-25 | |
| | |_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | | | | | Adding a V8.7 compatibility version number. | Hugo Herbelin | 2017-07-21 | |
| | |_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile) | Maxime Dénès | 2017-07-21 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | * | | No useless reallocation in Termops.collapse_appl. | Pierre-Marie Pédrot | 2017-07-21 | |
| | | | | | | | | | | | | | | | | * | | Allocation-friendly detyping of term arrays. | Pierre-Marie Pédrot | 2017-07-21 | |
| | * | | | | | | | | | | | | | | | | | PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it. | Maxime Dénès | 2017-07-21 | |
| | | | | | | | | | | | * | | | | | | | Add [opam update] and online repository to gitlab CI script. |  Gaëtan Gilbert | 2017-07-21 | |
| | | | | | | | | | | | | |_|_|_|/ / | | | | | | | | | | | |/| | | | | | ||||
| | | | | | | | | | | | | | | | * | | Alternate way of doing timing on ci |  Jason Gross | 2017-07-21 | |
| | | | | | | | | | | | | | | | * | | Separate make from python script for HoTT | Jason Gross | 2017-07-21 | |
| | | | | | | | | | | | | | | | * | | Display timing data travis for various projects | Jason Gross | 2017-07-21 | |
| | | | | | | | | | | | | |_|_|/ / | | | | | | | | | | | |/| | | | | ||||
| | * | | | | | | | | | | | | | | | Install time command under Cygwin (required for timing scripts). | Maxime Dénès | 2017-07-21 | |
| | | | | * | | | | | | | | | | | | Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720) | Pierre Letouzey | 2017-07-20 | |
| | | | | | |_|_|_|_|_|/ / / / / | | | | |/| | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | Merge PR #892: Improve do_split option of typeclass resolution | Maxime Dénès | 2017-07-20 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | ||||
| | | * | | | | | | | | | | | | | fake_ide: do as coqide to find out coqtop path |  Enrico Tassi | 2017-07-20 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |