aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
| | | | | | | | | | | | | | | | * | | | | Add test for NonCumulative inductivesGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | * | | | | Issue error on monomorphic cumulative inductivesGravatar Amin Timany2017-07-31
| | | | | | | | | | | | | | | | | |_|/ / | | | | | | | | | | | | | | | | |/| | |
* | | | | | | | | | | | | | | | | | | | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #746: Timing on ci via coq_makefile for various projectsGravatar Maxime Dénès2017-07-31
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | | | | | Drop paragraph mentioning Addendum as separate doc.Gravatar Théo Zimmermann2017-07-29
| | | | * | | | | | | | | | | | | | | | | closing bug 5315Gravatar Julien Forest2017-07-29
| |_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | Merge PR #923: [api] Fix base_include LTAC parts.Gravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #889: Removing template polymorphism for definitions.Gravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #888: Stronger kernel typesGravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #823: Async off in Windows by default in CoqIDEGravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #782: Update API for fiatGravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | | | * | Fix some coq-tex errors in the reference manual.Gravatar Guillaume Melquiond2017-07-28
| | | | | | | | | | | | | | | | | | | | | * | | | Fix documentation of Hint Mode (bug #4911).Gravatar Guillaume Melquiond2017-07-28
| | | | | | | | | | | | | | | | | | | | | | |/ / | | | | | | | | | | | | | | | | | | | | | |/| |
| | | | | | | | | | | | | | | | | | | | * / | | Fix shuffled documentation.Gravatar Guillaume Melquiond2017-07-28
| | | | | | | | | | | | | | | | | | | | |/ / /
* | | | | | | | | | | | | | | | | | | | | | | Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceGravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | * | | | Add missing paragraph to introductionGravatar Benjamin Pierce2017-07-27
| | | | | | | | | | | | | | | | | | | | |/ / /
| | | | | | | | | | | | | | | | | | | * / / / Fixing bug #5671 (specialize unclean wrt Metas).Gravatar Hugo Herbelin2017-07-27
| | | | | | | | | | | | | | | | | | | |/ / /
| | | | | | | | | | | | | | | | | * | | | | Extraction.tex: mention the possible "From Coq Require Extraction"Gravatar letouzey2017-07-27
| | | | | | | | | | | | | | | | | * | | | | Extraction TestCompile documented + mentionned in CHANGESGravatar Pierre Letouzey2017-07-27
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * | | | test-suite: more use of the new command Extraction TestCompileGravatar Pierre Letouzey2017-07-27
| | | | | | | | | * | | | | | | | | | | | [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| | | | | | | | | | |_|_|_|_|_|_|_|/ / / | | | | | | | | | |/| | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | [make] remove compat5 file.Gravatar Emilio Jesus Gallego Arias2017-07-27
| | | | | | | | | | |_|_|_|_|_|/ / / / | | | | | | | | | |/| | | | | | | | |
| | | | | | * | | / | | | | | | | | | [api] Fix base_include LTAC parts.Gravatar Emilio Jesus Gallego Arias2017-07-27
| | | | | | | |_|/ / / / / / / / / / | | | | | | |/| | | | | | | | | | |
| | | | | | | | * | | | | | | | | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | | | | * | | | | | | | | | | | Fix TypeclassDebug.out after conflicting PR mergesGravatar Matthieu Sozeau2017-07-26
| |_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | | 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 14:32:14 +0000