aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-26Properly handling toplevel recursive definitions.Pierre-Marie Pédrot
2017-07-26Merge PR #750: Remove deprecated options of ./configure in 8.8Maxime Dénès
2017-07-26Exporting some basic tactics from Ltac1.Pierre-Marie Pédrot
2017-07-26make sure that API-leaks cannot be reintroduced by mistakeMatej Košík
2017-07-26Bugfix: wrong access to non-constant constructor compilation.Pierre-Marie Pédrot
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
2017-07-25[api] Put modules in order in API.{mli,ml}Emilio Jesus Gallego Arias
2017-07-25Generalizing patterns in fun bindings.Pierre-Marie Pédrot
2017-07-25Adding -print-version in addition to -print-version for consistency.Hugo Herbelin
2017-07-25Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Pierre Letouzey
2017-07-24Adding a few primitive functions.Pierre-Marie Pédrot
2017-07-24Correctly pushing variables for tuple patterns.Pierre-Marie Pédrot
2017-07-24Properly handle parsing of list patterns.Pierre-Marie Pédrot
2017-07-24Fix typo.Pierre-Marie Pédrot
2017-07-24Removing a spurious file.Pierre-Marie Pédrot
2017-07-24Filling the README.Pierre-Marie Pédrot
2017-07-24Adding quick-n-dirty tests.Pierre-Marie Pédrot
2017-07-24Fix library hardwired prefix.Pierre-Marie Pédrot
2017-07-24Turning the ltac2 subfolder into a standalone plugin.Pierre-Marie Pédrot
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-21Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)Maxime Dénès
2017-07-21No useless reallocation in Termops.collapse_appl.Pierre-Marie Pédrot
2017-07-21Allocation-friendly detyping of term arrays.Pierre-Marie Pédrot
2017-07-21PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.Maxime Dénès
2017-07-21Add [opam update] and online repository to gitlab CI script.Gaëtan Gilbert
2017-07-21Alternate way of doing timing on ciJason Gross
2017-07-21Separate make from python script for HoTTJason Gross
2017-07-21Display timing data travis for various projectsJason Gross
2017-07-21Install time command under Cygwin (required for timing scripts).Maxime Dénès
2017-07-20Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Pierre Letouzey
2017-07-20Merge PR #892: Improve do_split option of typeclass resolutionMaxime Dénès
2017-07-20fake_ide: do as coqide to find out coqtop pathEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 04:27:41 +0000