aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-08-01Merge PR #917: Moving --print-version to -print-version for consistency.Maxime Dénès
2017-08-01Merge PR #913: Less allocations in DetypingMaxime Dénès
2017-08-01Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Maxime Dénès
2017-08-01Merge PR #893: Removing default evar-normalization for ARGUMENT EXTEND.Maxime Dénès
2017-08-01Merge PR #834: Adding support for recursive notations of the form "x , .. , y...Maxime Dénès
2017-08-01Merge PR #806: closing bug 5315Maxime Dénès
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-31Merge PR #746: Timing on ci via coq_makefile for various projectsMaxime Dénès
2017-07-29closing bug 5315Julien Forest
2017-07-28Merge PR #923: [api] Fix base_include LTAC parts.Maxime Dénès
2017-07-28Merge PR #889: Removing template polymorphism for definitions.Maxime Dénès
2017-07-28Merge PR #888: Stronger kernel typesMaxime Dénès
2017-07-28Merge PR #823: Async off in Windows by default in CoqIDEMaxime Dénès
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-28Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceMaxime Dénès
2017-07-27[toplevel] Remove long ago deprecated and NOOP options.Emilio Jesus Gallego Arias
2017-07-27[api] Fix base_include LTAC parts.Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Fix TypeclassDebug.out after conflicting PR mergesMatthieu Sozeau
2017-07-26adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...Pierre Letouzey
2017-07-26Extraction: reduce primitive projections in types (fix bug 4709)Pierre Letouzey
2017-07-26Add a comment regarding the specialization of the combinator in Detyping.Pierre-Marie Pédrot
2017-07-26Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Maxime Dénès
2017-07-26Merge PR #910: Add [opam update] and online repository to gitlab CI script.Maxime Dénès
2017-07-26Removing default evar-normalization for ARGUMENT EXTEND.Pierre-Marie Pédrot
2017-07-26Merge PR #886: Fixing what was presumably a typo in the naming conventions fileMaxime Dénès
2017-07-26Merge PR #902: Only perform profile initialization and printing when the flag...Maxime Dénès
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-26Merge PR #894: Fixing a little location bug with recursive bindersMaxime Dénès
2017-07-26Merge PR #882: Adding a V8.7 compatibility version number.Maxime Dénès
2017-07-26Avoiding a variable shadowing in the kernel.Pierre-Marie Pédrot
2017-07-26Statically ensuring that inlined entries out of the kernel have no effects.Pierre-Marie Pédrot
2017-07-26Further simplication: do not recreate entries for side-effects.Pierre-Marie Pédrot
2017-07-26Remove a horrendous hack in Declare to retrieve exported side-effects.Pierre-Marie Pédrot
2017-07-26More precise type of entries capturing their lack of side-effects.Pierre-Marie Pédrot
2017-07-26Using a record type for Cooking.result.Pierre-Marie Pédrot
2017-07-26More precise type for universe entries.Pierre-Marie Pédrot
2017-07-26Merge PR #885: Removing a dummy parameter in some FMapPositive statements.Maxime Dénès
2017-07-26Adding support for recursive notations of the form "x , .. , y , z".Hugo Herbelin
2017-07-26Merge PR #868: Fix debug trace of typeclasses eauto.Maxime Dénès
2017-07-26Merge PR #845: Add Z.mod_div lemma to standard library.Maxime Dénès
2017-07-26Merge PR #905: [api] Remove type equalities from API.Maxime Dénès
2017-07-26Merge PR #857: Extraction: various fixes related with bug 4720Maxime Dénès
2017-07-26Merge PR #859: Extraction TestCompileMaxime Dénès
2017-07-26Merge PR #808: [api] Put some order in API.mliMaxime Dénès
2017-07-26Merge PR #750: Remove deprecated options of ./configure in 8.8Maxime Dénès
2017-07-26make sure that API-leaks cannot be reintroduced by mistakeMatej Košík
2017-07-25Makefile.ide: restore a coqide-binaries rule (fix bug 5667)Pierre Letouzey
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias