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