aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-29Fast environment lookup for rels.Pierre-Marie Pédrot
2017-12-29Adding skewed lists.Pierre-Marie Pédrot
2017-12-27Merge PR #6102: Fix #5998: AppVeyor package building is currently failingMaxime Dénès
2017-12-27Re-enable package building and artefact storage.Maxime Dénès
2017-12-27Fix #5998: AppVeyor package building is currently failingMaxime Dénès
2017-12-27Merge PR #6507: [ide] [doc] Document tweak to Query call.Maxime Dénès
2017-12-27Merge PR #6504: Fix overlay selection for Circle CI.Maxime Dénès
2017-12-27Merge PR #6040: Making coq_makefile usage consistent with what it claims + po...Maxime Dénès
2017-12-27Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Maxime Dénès
2017-12-27Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.Maxime Dénès
2017-12-27Merge PR #6443: [vernac] Cleanup of do_definition.Maxime Dénès
2017-12-27Merge PR #6495: Remove syntax for classification in TACTIC EXTEND.Maxime Dénès
2017-12-27Merge PR #6494: Remove legacy Value.normalize function.Maxime Dénès
2017-12-27Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...Maxime Dénès
2017-12-27Merge PR #6473: Fix warning about shadowing a global name.Maxime Dénès
2017-12-26[ide] [doc] Document tweak to Query call.Emilio Jesus Gallego Arias
2017-12-26Fix overlay selection for Circle CI.Gaëtan Gilbert
2017-12-26Delete old overlays (leaving example)Gaëtan Gilbert
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-23[lib] Split auxiliary libraries into Coq-specific and general.Emilio Jesus Gallego Arias
2017-12-23Registering a printing handler in coq_makefile.Hugo Herbelin
2017-12-23Forbidding -o and -f in input file of coq_makefile.Hugo Herbelin
2017-12-23Removing failure of coq_makefile on no arguments.Hugo Herbelin
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-22Remove syntax for classification in TACTIC EXTEND.Maxime Dénès
2017-12-22Remove legacy Value.normalize function.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-21Merge code paths in interp_definition and cleanup a bit.Gaëtan Gilbert
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 warning about shadowing a global name.Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 17:30:02 +0000