| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-15 | Merge PR #8589: Correct some spelling errors (continued) | Emilio Jesus Gallego Arias | |
| 2018-10-15 | Merge PR #8717: Lemmas, DeclareDef: internal reorganization of code ↵ | Emilio Jesus Gallego Arias | |
| highlighting what can be shared | |||
| 2018-10-15 | Mini-factorization preparing unification. | Hugo Herbelin | |
| 2018-10-15 | Make 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-15 | DeclareDef: 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-15 | Merge PR #8716: Lemmas: Little simplification of artificially convoluted code | Emilio Jesus Gallego Arias | |
| 2018-10-15 | Correct some spelling errors | Benjamin 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-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 | A useless occurrence of Global.env. | Hugo Herbelin | |
| 2018-10-14 | Parameterizing default inhabitant for impossible cases with an environment. | Hugo Herbelin | |
| 2018-10-14 | Removing a call to Global.env in evarsolve. | Hugo Herbelin | |
| 2018-10-14 | Removing useless call to Global.env in check_and_clear_in_constr. | Hugo Herbelin | |
| 2018-10-14 | Passing env functionally in move_hyp and insert_decl_in_named_context. | Hugo Herbelin | |
| 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-13 | Add unicode category LM | Mirai IKEBUCHI | |
| 2018-10-12 | Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml. | Hugo Herbelin | |
| This is to move a standard combinator to the place it belongs to. An alternative could have been to put it in termops.ml, but termops.ml is now about econstr, so, even if it makes the kernel "bigger", constr.ml seems to be the best place for this combinator. After all, this combinator is canonical. | |||
| 2018-10-12 | Merge PR #8714: Documenting -arg in _CoqProject. | Théo Zimmermann | |
| 2018-10-12 | [ci] [appveyor] Disable validate target. | Emilio Jesus Gallego Arias | |
| Not a big point on running the checker on Appveyor I think, this will save a bunch of time and improve reliability. | |||
| 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 | A state-free version of is_polymorphic. | Hugo Herbelin | |
| 2018-10-11 | Adding 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-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 | [ci] [appveyor] Enable cache for builds. | Emilio Jesus Gallego Arias | |
| We cache CYGWIN and OPAM. Current cygwin install is not deterministic but should do the job in the scope of this job. | |||
| 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 | Fix for coq/coq#8515 (command driven attributes) | Gaëtan Gilbert | |
| 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 | Also clean up the checker w.r.t. unused closure data. | Pierre-Marie Pédrot | |
| 2018-10-11 | Clean up CClosure code. | Pierre-Marie Pédrot | |
| We take advantage of the separation of implementation from CBV to remove constant code. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |