aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-16Merge PR #8742: [clib] Remove Array functions available in OCaml 4.05.0Pierre-Marie Pédrot
2018-10-16Merge PR #8059: Simplify code for [Definition := Eval ...]Matthieu Sozeau
2018-10-16Merge PR #8691: Remove some dead code in nsatz and micromega pluginsthery
2018-10-16[clib] Remove Array functions available in OCaml 4.05.0Emilio Jesus Gallego Arias
2018-10-16[test-suite] Update csdp cacheVincent Laporte
2018-10-16[micromega] remove dead codeVincent Laporte
2018-10-16[nsatz] remove dead codeVincent Laporte
2018-10-16Merge PR #8695: Adding a functional version of constant- and ↵Pierre-Marie Pédrot
mind_of_delta_kn + functional version of is_polymorphic
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
Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code.
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
We chose to stick to the most general possible API, even though the macro will not make full use of the possibilities. It makes explicit the various data expected to be provided in an orthogonal way.
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
Those optional arguments did not really make sense. It was pretty clear from our code base, as all instances where triplicating the same type for TYPED, RAW_TYPED and GLOB_TYPED.
2018-10-15Merge PR #8689: A few useless accesses to the global environment in ↵Pierre-Marie Pédrot
pretyping and engine
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 ↵Emilio Jesus Gallego Arias
highlighting what can be shared
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
This is a theoretical change of semantics in the presence of commands generating a "hook", such as "Coercion c := ...", or "SubClass", or "Canonical Structure". However, none of these commands have a "Discharge" effect, so the case was not used.
2018-10-15DeclareDef: Reorganizing declaration of definitions in a more structured way.Hugo Herbelin
In particular, we highlight the similarities and differences between local and global definitions.
2018-10-15Merge PR #8716: Lemmas: Little simplification of artificially convoluted codeEmilio Jesus Gallego Arias
2018-10-15Correct some spelling errorsBenjamin Barenblat
Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
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
Fixes #8337
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
TOC, ...
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
"Declaration" hooks can be polymorphic on their return type, however this facility doesn't seem used in the codebase. We thus remove the polymorphism with the hope to be able to reify the control later on.
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 ↵Emilio Jesus Gallego Arias
interning/printing
2018-10-11Merge PR #8594: Miscellaneous refinements and cleaning of module printingEmilio Jesus Gallego Arias
2018-10-11Documenting -arg in _CoqProject.Hugo Herbelin
We follow Proof General documentation, section 11.2 "Using the Coq project file".
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 ↵Théo Zimmermann
Dune.
2018-10-11[coq_dune] Abstract path operations wrt directory separator.Emilio Jesus Gallego Arias
Even if cosmetic, this is useful for window-based hosts.
2018-10-11[vernac] Remove unused `start_hook` `save_hook` from Lemmas.Emilio Jesus Gallego Arias
These hooks are 10-years old and long unused I think.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:07:08 +0000