aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-07Add empty compat file for Coq 8.8Jason Gross
2018-03-07Merge PR #6744: Add String.concatMaxime Dénès
2018-03-07Merge PR #6932: [stdlib] Do not use deprecated notationsMaxime Dénès
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Maxime Dénès
2018-03-07Merge PR #6922: Remove outdated information regarding the FAQ.Maxime Dénès
2018-03-07Merge PR #6374: [toplevel] Modify printing goal strategy.Maxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-07Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Maxime Dénès
2018-03-06Add CHANGES and man entry for coqdep learning _CoqProject.Gaëtan Gilbert
2018-03-06Closes #6830: coqdep reads options and files from _CoqProject.Gaëtan Gilbert
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
2018-03-06Extraction: switch to EConstr.t as the central type to extract from.Pierre Letouzey
2018-03-06romega: get rid of EConstr.UnsafePierre Letouzey
2018-03-06document -profile in dev/doc/setup.txtEnrico Tassi
2018-03-06Standard headers for C and Python.Maxime Dénès
2018-03-06[stdlib] Do not use deprecated notationsVincent Laporte
2018-03-06Add some missing flushes in configure.Maxime Dénès
2018-03-06Hack to make bignum build on windowsEnrico Tassi
2018-03-06build: win: turn off build/installation of gnu MakeEnrico Tassi
2018-03-06Clean-up remove always false useeager argument.Théo Zimmermann
2018-03-06Remove outdated information regarding the FAQ.Théo Zimmermann
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-06Merge PR #6917: Fix failing packaging job.Maxime Dénès
2018-03-06[compat] Remove "Discriminate Introduction"Emilio Jesus Gallego Arias
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Maxime Dénès
2018-03-06Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Maxime Dénès
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-06Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Maxime Dénès
2018-03-05[toplevel] Modify printing goal strategy.Emilio Jesus Gallego Arias
2018-03-05Fix failing packaging job.Théo Zimmermann
2018-03-05Remove NOPLUGINDOCS optionmrmr1993
2018-03-05Add empty description for @raise statements to satisfy ocamldocmrmr1993
2018-03-05Escape curly braces in ocamldoc commentmrmr1993
2018-03-05Separate vim/emacs fold markers from ocamldoc commentsmrmr1993
2018-03-05Build docs for plugins by default, add NOPLUGINDOCS flag to disablemrmr1993
2018-03-05Change non-documentation comment from ocamldoc stylemrmr1993
2018-03-05Fix formatting of some ocamldoc comments to reduce warningsmrmr1993
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Remove non-existent dependencymrmr1993
2018-03-05Tweak comments to fix ocamldoc errorsmrmr1993
2018-03-05Tidy up ml-doc outut, give it a separate output directorymrmr1993
2018-03-05Use computed deps to generate ml-doc and use implicit mli-doc depsmrmr1993
2018-03-05[build] Simpler byte/opt toplevel build.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:08:32 +0000