| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-05 | Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks. | Pierre-Marie Pédrot | |
| 2018-12-04 | Document undocumented flags and options | Jim Fehrle | |
| Also remove a few undocumented settings | |||
| 2018-11-30 | [vernac] [hooks] Refactor towards optional hooks. | Emilio Jesus Gallego Arias | |
| We make `declaration_hook`s optional arguments everywhere, and thus we avoid some "fake" functions having to be passed. This identifies positively the code really using hooks [funind, rewrite, coercions, program, and canonicals] and helps moving toward some hope of reification. | |||
| 2018-11-30 | Merge PR #9102: [ltac] Remove aliases already present in the lower layers. | Pierre-Marie Pédrot | |
| 2018-11-30 | Merge PR #9064: [gramlib] Minor cleanups: | Pierre-Marie Pédrot | |
| 2018-11-28 | Merge PR #9070: [ssreflect] Export more parsing witnesses. | Enrico Tassi | |
| 2018-11-28 | [ltac] Remove aliases already present in the lower layers. | Emilio Jesus Gallego Arias | |
| We remove a few aliases present in the lower layers [`Genintern/Tactypes`] from `Tacexpr`. IMHO this enlarges the API for no good purpose, and difficults analysis. | |||
| 2018-11-27 | [gramlib] Minor cleanups: | Emilio Jesus Gallego Arias | |
| - remove duplicate type definitions `gram_assoc`, `gram_position`, - make global `warning_verbose` variable into a parameter. | |||
| 2018-11-27 | Merge PR #9046: Goptions.declare_* functions return unit instead of a ↵ | Emilio Jesus Gallego Arias | |
| write_function | |||
| 2018-11-27 | Merge PR #8850: Private universes for opaque polymorphic constants. | Matthieu Sozeau | |
| 2018-11-26 | [ssreflect] Export more parsing witnesses. | Emilio Jesus Gallego Arias | |
| This is needed in order to serialize ssreflect programs properly, similar to #6795. | |||
| 2018-11-23 | Remove the unsafe camlp5 API from the Coq codebase. | Pierre-Marie Pédrot | |
| 2018-11-23 | Only use Coq API in coqpp. | Pierre-Marie Pédrot | |
| 2018-11-23 | Local universes for opaque polymorphic constants. | Gaëtan Gilbert | |
| 2018-11-23 | s/let _ =/let () =/ in some places (mostly goptions related) | Gaëtan Gilbert | |
| 2018-11-21 | Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlib | Enrico Tassi | |
| 2018-11-21 | [legacy proof engine] Remove some cruft. | Emilio Jesus Gallego Arias | |
| We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps. | |||
| 2018-11-21 | [gramlib] [build] Switch make-based system to packed gramlib | Emilio Jesus Gallego Arias | |
| This makes the make-based build system stop linking to Camlp5's gramlib and instead links to our own gramlib. We use the style done in the packing of `Stdlib` in OCaml 4.07. As to introduce a minimal amount of noise in history we use an autogenerated `gramlib__pack` directory. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2018-11-20 | Merge PR #9017: Remove SSR profiling | Enrico Tassi | |
| 2018-11-20 | Merge PR #7925: Clean transparent state | Maxime Dénès | |
| 2018-11-19 | Merge PR #8987: Deprecate hint declaration/removal with no specified database | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #9003: [vernacextend] Consolidate extension points API | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8902: [ltac] Use CAst nodes in the tactic AST. | Pierre-Marie Pédrot | |
| 2018-11-19 | Rename TranspState into TransparentState. | Pierre-Marie Pédrot | |
| 2018-11-19 | Proper record type and accessors for transparent states. | Pierre-Marie Pédrot | |
| This is documented in dev/doc/changes.md. | |||
| 2018-11-19 | Move transparent_state to its own module. | Pierre-Marie Pédrot | |
| 2018-11-17 | [vernacextend] Consolidate extension points API | Emilio Jesus Gallego Arias | |
| We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`. | |||
| 2018-11-17 | [pfedit] Remove cook_proof stub. | Emilio Jesus Gallego Arias | |
| This is barely used and not very useful, clients should use the close_proof API directly. | |||
| 2018-11-17 | [ltac] Use CAst nodes in the tactic AST. | Emilio Jesus Gallego Arias | |
| This provides several advantages to people serializing tactic scripts. Appearance of the involved constructors is common enough as to bother to submit this PR. | |||
| 2018-11-16 | Remove SSR profiling | Jim Fehrle | |
| Deletes the SsrProfiling and SsrMatchingProfiling options | |||
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-14 | ssr: rewrite: do resolve TC once and forall at the very end | Enrico Tassi | |
| 2018-11-14 | ssr: elim: do resolve TC once and forall at the very end | Enrico Tassi | |
| 2018-11-14 | ssrcommon: API to call resolve_tyclasses on a term | Enrico Tassi | |
| 2018-11-14 | ssrmatching: unify_HO does not resolve type classes | Enrico Tassi | |
| 2018-11-14 | Deprecate hint declaration/removal with no specified database | Maxime Dénès | |
| Previously, hints added without a specified database where implicitly put in the "core" database, which was discouraged by the user manual (because of the lack of modularity of this approach). | |||
| 2018-11-13 | [vernac] Rename Vernacinterp to Vernacextend and move extension functions there. | Emilio Jesus Gallego Arias | |
| This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API. | |||
| 2018-11-12 | Merge PR #8972: Fix #4771: Substitution of inline global reference in ↵ | Pierre-Marie Pédrot | |
| tactics is broken | |||
| 2018-11-12 | Merge PR #8938: [Plugins] Remove some dead code | Pierre-Marie Pédrot | |
| 2018-11-12 | Fix #4771: Substitution of inline global reference in tactics is broken | Maxime Dénès | |
| 2018-11-07 | [Funind plugin] Remove some dead code | Vincent Laporte | |
| 2018-11-07 | [Firstorder plugin] Remove some dead code | Vincent Laporte | |
| 2018-11-07 | [CC plugin] Remove dead code | Vincent Laporte | |
| 2018-11-07 | [R syntax plugin] Remove some dead code | Vincent Laporte | |
| 2018-11-07 | [doc] nodes in ssr are monospace | Enrico Tassi | |
| 2018-11-07 | multi line comments don't have a title | Enrico Tassi | |
| 2018-11-07 | [doc] adapt comments in plugins/ssr/*.v to coqdoc style | Enrico Tassi | |
| 2018-11-06 | [checker] Refactor by sharing code with the kernel | Maxime Dénès | |
| For historical reasons, the checker was duplicating a lot of code of the kernel. The main differences I found were bug fixes that had not been backported. With this patch, the checker uses the kernel as a library to serve the same purpose as before: validation of a `.vo` file, re-typechecking all definitions a posteriori. We also rename some files from the checker so that they don't clash with kernel files. | |||
| 2018-11-06 | Merge PR #8556: [ssr] use tclDISPATCH for IPatDispatch (fix #8544) | Maxime Dénès | |
| 2018-11-05 | Merge PR #8515: Command driven attributes | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |