aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-29Add instructions for debugging from the command line (and in Windows)Jim Fehrle
2017-12-22Merge PR #6465: Gitlab touchupMaxime Dénès
2017-12-22Merge PR #6469: No universe constraints in Let definitionsMaxime Dénès
2017-12-22Merge PR #6318: Separate vernac controls and regular commands.Maxime Dénès
2017-12-22Merge PR #6484: Update README and CONTRIBUTING to mention the wiki and FAQ.Maxime Dénès
2017-12-22Merge PR #6485: Fix badges.Maxime Dénès
2017-12-22Merge PR #6445: [stm] [ide protocol] Allow to include several commands on query.Maxime Dénès
2017-12-22Merge PR #6222: Share computation of unifiable evarsMaxime Dénès
2017-12-21Fix badges.Théo Zimmermann
2017-12-21Update README and CONTRIBUTING to mention the wiki and FAQ.Théo Zimmermann
2017-12-21Merge PR #6474: Fix CI with parallel make (messed up dependencies)Maxime Dénès
2017-12-21Fix CI with parallel make (messed up dependencies)Gaëtan Gilbert
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-12-20Merge PR #6377: Removal of the FAQ LaTex document.Maxime Dénès
2017-12-20Merge PR #6470: Fix typo in the refman.Maxime Dénès
2017-12-20Merge PR #6449: Let definitions must not contain side-effects when reaching t...Maxime Dénès
2017-12-20Merge PR #6468: Fix order of let-in representation comment.Maxime Dénès
2017-12-20Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge).Maxime Dénès
2017-12-20Merge PR #6234: Make the micromega extraction check a regular output test.Maxime Dénès
2017-12-19Fix ltacprof_abstract (I think because of #6411 parallel merge).Gaëtan Gilbert
2017-12-19Fix typo in the refman.Théo Zimmermann
2017-12-19Let definitions do not create new universe constraints.Pierre-Marie Pédrot
2017-12-19Merge PR #6400: Circle CIMaxime Dénès
2017-12-19Specific type for section definition entries.Pierre-Marie Pédrot
2017-12-19Fix order of let-in representation comment.Jasper Hugunin
2017-12-18Gitlab: don't ./configure in documentation jobGaëtan Gilbert
2017-12-18Merge PR #6436: Fix #5368: Canonical structure unification fails.Maxime Dénès
2017-12-18Merge PR #6447: [make] More build fixes for static plugins and ocamlfind.Maxime Dénès
2017-12-18Merge PR #6284: Warning for absolute name masking (deprecated, should become ...Maxime Dénès
2017-12-18Merge PR #6381: A version of [time] that works on constr evaluationMaxime Dénès
2017-12-18Merge PR #6406: Make [abstract] nodes show up in the Ltac profileMaxime Dénès
2017-12-18Merge PR #6380: Add tactics to reset and display the Ltac profileMaxime Dénès
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Maxime Dénès
2017-12-18Merge PR #6305: Build with windows line endingsMaxime Dénès
2017-12-18Merge PR #6217: Do dependencies in 1 command per file class.Maxime Dénès
2017-12-18Removing the FAQ, which has been moved to the GitHub wiki for thisMatt Quinn
2017-12-18Merge PR #6453: [doc] Nit on the manual.Maxime Dénès
2017-12-18Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingMaxime Dénès
2017-12-18Merge PR #6419: [vernac] Split `command.ml` into separate files.Maxime Dénès
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
2017-12-17[doc] Nit on the manual.Emilio Jesus Gallego Arias
2017-12-16Fix build fileJim
2017-12-16For bug 6249, Segmentation fault when building Coq on Windows 10.Jim
2017-12-16Let definitions must not contain side-effects when reaching the kernel.Pierre-Marie Pédrot
2017-12-16[make] More build fixes for static plugins and ocamlfind.Emilio Jesus Gallego Arias
2017-12-16[stm] [ide protocol] Allow to include several commands on query.Emilio Jesus Gallego Arias
2017-12-15Overlay for unimath.Gaëtan Gilbert
2017-12-15Do dependencies in 1 command per file class.Gaëtan Gilbert