aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-10-16[clib] Remove Array functions available in OCaml 4.05.0Emilio Jesus Gallego Arias
2018-10-16Merge PR #8695: Adding a functional version of constant- and mind_of_delta_kn...Pierre-Marie Pédrot
2018-10-16Merge PR #8733: Implement ARGUMENT EXTEND in coqppEmilio Jesus Gallego Arias
2018-10-15Documenting the transition from camlp5 to coqpp for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-15Implement ARGUMENT EXTEND in coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Providing a centralized API for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
2018-10-15Merge PR #8689: A few useless accesses to the global environment in pretyping...Pierre-Marie Pédrot
2018-10-15Merge PR #8589: Correct some spelling errors (continued)Emilio Jesus Gallego Arias
2018-10-15Merge PR #8717: Lemmas, DeclareDef: internal reorganization of code highlight...Emilio Jesus Gallego Arias
2018-10-15Mini-factorization preparing unification.Hugo Herbelin
2018-10-15Make code of `Lemmas.save` closer to the one of `DeclareDef.declare_definition`.Hugo Herbelin
2018-10-15DeclareDef: Reorganizing declaration of definitions in a more structured way.Hugo Herbelin
2018-10-15Merge PR #8716: Lemmas: Little simplification of artificially convoluted codeEmilio Jesus Gallego Arias
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-15Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type.Hugo Herbelin
2018-10-15Merge PR #8732: [ci] [sf] Remove sed hacks from the SF build.Gaëtan Gilbert
2018-10-14[ci] [sf] Remove sed hacks from the SF build.Emilio Jesus Gallego Arias
2018-10-14A useless occurrence of Global.env.Hugo Herbelin
2018-10-14Parameterizing default inhabitant for impossible cases with an environment.Hugo Herbelin
2018-10-14Removing a call to Global.env in evarsolve.Hugo Herbelin
2018-10-14Removing useless call to Global.env in check_and_clear_in_constr.Hugo Herbelin
2018-10-14Passing env functionally in move_hyp and insert_decl_in_named_context.Hugo Herbelin
2018-10-14Merge PR #8546: [ci] Allow bedrock to fail.Gaëtan Gilbert
2018-10-13Merge PR #8616: Include the full Table of Contents document in the on-screen ...Clément Pit-Claudel
2018-10-13Merge PR #8652: Add missing indexes for Hint Cut and Hint Mode.Clément Pit-Claudel
2018-10-12Merge PR #8714: Documenting -arg in _CoqProject.Théo Zimmermann
2018-10-12Merge PR #8665: Fix a few bugs in the checkerPierre-Marie Pédrot
2018-10-12Lemmas: Little simplification of artificially convoluted code.Hugo Herbelin
2018-10-11A state-free version of is_polymorphic.Hugo Herbelin
2018-10-11Adding a functional version of constant_of_delta_kn.Hugo Herbelin
2018-10-11[vernac] Remove unused abstraction from declaration_hook type.Emilio Jesus Gallego Arias
2018-10-11Merge PR #8703: [vernac] Remove unused `start_hook` `save_hook` from Lemmas.Hugo Herbelin
2018-10-11Merge PR #8680: Check that lambda/prod ast's have proper binders during inter...Emilio Jesus Gallego Arias
2018-10-11Merge PR #8594: Miscellaneous refinements and cleaning of module printingEmilio Jesus Gallego Arias
2018-10-11Documenting -arg in _CoqProject.Hugo Herbelin
2018-10-11Check that lambda/prod ast's have proper binders during interning/printing.Lasse Blaauwbroek
2018-10-11Merge PR #8702: [coq_dune] Abstract path operations wrt directory separator.Théo Zimmermann
2018-10-11Merge PR #8681: [dune] Fix and improve flags:Théo Zimmermann
2018-10-11Merge PR #8566: [dune] [test-suite] Support for running the test suite with D...Théo Zimmermann
2018-10-11[coq_dune] Abstract path operations wrt directory separator.Emilio Jesus Gallego Arias
2018-10-11[vernac] Remove unused `start_hook` `save_hook` from Lemmas.Emilio Jesus Gallego Arias
2018-10-11Merge PR #8698: [dune] Require that `plugin_base.dune` exists in plugin dirs.Théo Zimmermann
2018-10-11[dune] Add optimizing flags to release profile.Emilio Jesus Gallego Arias
2018-10-11Merge PR #8699: [quote] Remove spurious file after deletion of quote plugin.Théo Zimmermann
2018-10-11Merge PR #8697: [dune] Fix public name of tool: coq_tex -> coq-texThéo Zimmermann
2018-10-11Merge PR #8648: Add minimal CHANGES entry about deprecated compat notationsThéo Zimmermann
2018-10-11[dune] [test-suite] Support for running the test suite with Dune.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 08:07:25 +0000