| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-15 | Merge PR #8716: Lemmas: Little simplification of artificially convoluted code | Emilio Jesus Gallego Arias | |
| 2018-10-15 | Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type. | Hugo Herbelin | |
| 2018-10-15 | Merge 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-14 | Merge PR #8546: [ci] Allow bedrock to fail. | Gaëtan Gilbert | |
| 2018-10-13 | Merge PR #8616: Include the full Table of Contents document in the on-screen ↵ | Clément Pit-Claudel | |
| TOC, ... | |||
| 2018-10-13 | Merge PR #8652: Add missing indexes for Hint Cut and Hint Mode. | Clément Pit-Claudel | |
| 2018-10-12 | Merge PR #8714: Documenting -arg in _CoqProject. | Théo Zimmermann | |
| 2018-10-12 | Merge PR #8665: Fix a few bugs in the checker | Pierre-Marie Pédrot | |
| 2018-10-12 | Lemmas: Little simplification of artificially convoluted code. | 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-11 | Merge PR #8703: [vernac] Remove unused `start_hook` `save_hook` from Lemmas. | Hugo Herbelin | |
| 2018-10-11 | Merge PR #8680: Check that lambda/prod ast's have proper binders during ↵ | Emilio Jesus Gallego Arias | |
| interning/printing | |||
| 2018-10-11 | Merge PR #8594: Miscellaneous refinements and cleaning of module printing | Emilio Jesus Gallego Arias | |
| 2018-10-11 | Documenting -arg in _CoqProject. | Hugo Herbelin | |
| We follow Proof General documentation, section 11.2 "Using the Coq project file". | |||
| 2018-10-11 | Check that lambda/prod ast's have proper binders during interning/printing. | Lasse Blaauwbroek | |
| 2018-10-11 | Merge PR #8702: [coq_dune] Abstract path operations wrt directory separator. | Théo Zimmermann | |
| 2018-10-11 | Merge PR #8681: [dune] Fix and improve flags: | Théo Zimmermann | |
| 2018-10-11 | Merge 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. | |||
| 2018-10-11 | Merge 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 | |
| - In `release` profile, we use an optimizing set of flags. This will only affect to people using a Flambda-enabled OCaml. - We use the `_` pattern for flags that are common to all profiles. | |||
| 2018-10-11 | Merge PR #8699: [quote] Remove spurious file after deletion of quote plugin. | Théo Zimmermann | |
| 2018-10-11 | Merge PR #8697: [dune] Fix public name of tool: coq_tex -> coq-tex | Théo Zimmermann | |
| 2018-10-11 | Merge PR #8648: Add minimal CHANGES entry about deprecated compat notations | Théo Zimmermann | |
| 2018-10-11 | [dune] [test-suite] Support for running the test suite with Dune. | Emilio Jesus Gallego Arias | |
| 2018-10-11 | [configure] Use absolute path for prefix. | Emilio Jesus Gallego Arias | |
| 2018-10-11 | Merge PR #186: [RFC] Coqlib cleanup | Pierre-Marie Pédrot | |
| 2018-10-11 | Merge PR #8709: [test-suite] Use the right OCAMLPATH separator on Windows. | Vincent Laporte | |
| 2018-10-11 | [test-suite] Use the right OCAMLPATH separator on Windows. | Emilio Jesus Gallego Arias | |
| Hopefully this goes away when OCAMLPATH is properly handled by the build system. | |||
| 2018-10-11 | Merge PR #8161: Implement VERNAC EXTEND in coqpp | Maxime Dénès | |
| 2018-10-11 | Merge PR #8644: [build] enable warnings on kernel/% in make based builds | Maxime Dénès | |
| 2018-10-11 | Merge PR #8701: Fix build of Nix package with sandbox. | Vincent Laporte | |
| 2018-10-10 | Add minimal CHANGES entry about compat notations | Jason Gross | |
| 2018-10-10 | Fix build of Nix package with sandbox. | Théo Zimmermann | |
| One more place where we must patch shebangs. | |||
| 2018-10-10 | Merge PR #8384: Small fixes in attribute documentation. | Clément Pit-Claudel | |
| 2018-10-10 | [quote] Remove spurious file after deletion of quote plugin. | Emilio Jesus Gallego Arias | |
| For some reason PR #7894 left this spurious file; this is typical of a bad resolution of a merge, and while the file is innocuous it should go away. | |||
| 2018-10-10 | Miscellaneous refinements/cleaning of module printing. | Hugo Herbelin | |
| This refines the fix to #2169 by distinguishing the short and non-short printing modes. This prepares functionalization of printers by always passing env rather than setting env to None in short mode. This is not strictly necessary for the env which is not used for printing global references but it shall be more consistent in style when passing e.g. the nametab functionally. We however keep the fallback printer used in case of error while printing: due to missing registration of submodule fields in the nametab, printing with types does not work if there are references to an inner module. | |||
| 2018-10-10 | [dune] Require that `plugin_base.dune` exists in plugin dirs. | Emilio Jesus Gallego Arias | |
| `coq_dune` should not consider a directory as a plugin one if the `plugin_base.dune` file doesn't exists, as the generated `dune` file for that dir will try to include it. We have had problems with this in the past due to spurious dirs. | |||
| 2018-10-10 | [doc] [sphinx] Fix title levels. | Théo Zimmermann | |
| 2018-10-10 | Include all menu entries in the menu/short TOC so that users can view | Jim Fehrle | |
| menu options for all chapters without having to load a new chapter. Change "Introcution" title to "Introduction and Contents" | |||
| 2018-10-10 | Fix names for 2 entries in Flags, Options, Tables index. | Jim Fehrle | |
| 2018-10-10 | [dune] Tweaks on `tools/dune` | Emilio Jesus Gallego Arias | |
| - `coq_tex -> `coq-tex` - we build and intall `coqworkmgr` - remove some redundancy | |||
| 2018-10-10 | Merge PR #8692: [test-suite] Don't reset `OCAMLPATH`, but append to it. | Enrico Tassi | |
| 2018-10-10 | [coqlib] Rebindable Coqlib namespace. | Emilio Jesus Gallego Arias | |
| We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2018-10-10 | [test-suite] Don't reset `OCAMLPATH`, but append to it. | Emilio Jesus Gallego Arias | |
| This fixes an obvious bug introduced in #8602. | |||
| 2018-10-10 | Merge PR #8693: [test-suite] rename a file | Pierre-Marie Pédrot | |
| 2018-10-10 | [test-suite] rename a file | Vincent Laporte | |
| 2018-10-10 | Merge PR #8651: [dune] Provide an optimized build profile with inlining reports. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |