| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-21 | Merge PR #8998: [legacy proof engine] Remove some cruft. | Pierre-Marie Pédrot | |
| 2018-11-21 | [sphinx] Progress towards closing #7602: remove most objects without a body. | Théo Zimmermann | |
| Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter. | |||
| 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 #8948: [dune] Some tweaks to docs. | Théo Zimmermann | |
| 2018-11-20 | Merge PR #9035: [dune] Only build printers when the ltac plugin is available. | Théo Zimmermann | |
| 2018-11-20 | [dune] Only build printers when the ltac plugin is available. | Emilio Jesus Gallego Arias | |
| This fixes a problem reported by @Zimmi48 in #8948, IMHO we should be able to have a clean build of core Coq. | |||
| 2018-11-20 | Merge PR #8959: [dune] [ide] Install data files. | Enrico Tassi | |
| 2018-11-20 | Notations: Trying using a notation with or w/o removal of coercions. | Hugo Herbelin | |
| Preferring a notation which does require a delimiter, depending on whether the coercion is removed or not, was done for primitive tokens. We do it for all notations. | |||
| 2018-11-20 | Merge PR #9016: PRINT_LOGS=1 in appveyor test suite run | Enrico Tassi | |
| 2018-11-20 | Merge PR #9017: Remove SSR profiling | Enrico Tassi | |
| 2018-11-20 | Merge PR #9033: gitlab: Install stdlib doc in build:base | Emilio Jesus Gallego Arias | |
| 2018-11-20 | Add a check that the return stack of an FProd is indeed empty. | Pierre-Marie Pédrot | |
| 2018-11-20 | Use a closure for the domain argument of FProd. | Pierre-Marie Pédrot | |
| The use of a term is not needed for the fast typing algorithm of the application case, so this tweak brings the best of both worlds. | |||
| 2018-11-20 | More efficient implementation of type_of_apply. | Pierre-Marie Pédrot | |
| 2018-11-20 | Do not wrap FProd return types in a closure. | Pierre-Marie Pédrot | |
| There is little point to this as the type is dependent on an open value and is never computed further. | |||
| 2018-11-20 | gitlab: Install stdlib doc in build:base | Gaëtan Gilbert | |
| Looks like we forgot to adapt this when we split off the sphinx job and stopped using -with-doc yes. | |||
| 2018-11-20 | Merge PR #9031: Rename gh->bug_ test files | Emilio Jesus Gallego Arias | |
| 2018-11-20 | Merge PR #8982: [proof] Provide better control of "open proofs" exceptions. | Pierre-Marie Pédrot | |
| 2018-11-20 | Merge PR #9002: [pfedit] Remove `start_proof` stub from `Pfedit` | Pierre-Marie Pédrot | |
| 2018-11-20 | Rename gh->bug_ test files | Gaëtan Gilbert | |
| 2018-11-20 | dune: link kernel in checker instead of copying files | Gaëtan Gilbert | |
| This allows to use the nice printers with constrextern etc, and since we were copying everything we're not linking any more than previously. Also the dune file is simpler without the copies. | |||
| 2018-11-20 | Fix dune-dbg using checker/main -> checker/coqchk | Gaëtan Gilbert | |
| 2018-11-20 | Merge PR #7925: Clean transparent state | Maxime Dénès | |
| 2018-11-19 | Minor update to micromega.rst | soraros | |
| 2018-11-19 | [pfedit] Remove `start_proof` stub from `Pfedit` | Emilio Jesus Gallego Arias | |
| This way we only have 2 `start_proof` entries, in `Lemmas` and `Proof_global`; which they should be unified / brought closer in the future. | |||
| 2018-11-19 | Merge PR #8987: Deprecate hint declaration/removal with no specified database | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge remote-tracking branch 'origin/pr/84' | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #9003: [vernacextend] Consolidate extension points API | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #9026: [Documentation/Combined Scheme] Typo | Théo Zimmermann | |
| 2018-11-19 | Typo: comment does not match code | Olivier Laurent | |
| 2018-11-19 | Adding a module to manipulate Ltac1 values. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8894: Print full binders in subtyping incompatible polymorphism error. | 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 | Merge PR #9001: [options] Remove deprecated option automatic introduction. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8999: [pfedit] Remove cook_proof stub. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #9023: [gramlib] Remove unused alias. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #9013: Do not Export the init modules | Pierre-Marie Pédrot | |
| 2018-11-19 | Fix dune checker file. | Pierre-Marie Pédrot | |
| 2018-11-19 | Adding overlays. | 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-19 | Add a function to generate fresh reference instances. | Pierre-Marie Pédrot | |
| 2018-11-19 | Add a Char module. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8451: Print Universes Subgraph | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #7881: Reimplement Store using Dyn | Pierre-Marie Pédrot | |
| 2018-11-19 | [gramlib] Remove unused alias. | Emilio Jesus Gallego Arias | |
| No effect on actual code. | |||
| 2018-11-19 | [proof] Provide better control of "open proofs" exceptions. | Emilio Jesus Gallego Arias | |
| This is inspired and an alternative to #8981. We consolidate the "open proof" exception, allowing clients to explicitly capture it and removing some ugly duplicated code in the way. The `Solve Obligation tac` semantics are then tweaked as to removed the wide-scope "catch-all" and indeed will now relay errors in `tac` as it will only absorb tactics that don't error but fail to close the goal such as `auto`. For the rest of the cases, we introduce a warning, and may move to a full error in later releases. We also remove an unnecessary `tclCOMPLETE` call to code that will actually call `close_proof`. In this case, it is better to delegate error management to the core function. Some error messages have changed [as we consolidate two error paths] so this PR may require adjustment in that area. | |||
| 2018-11-18 | [options] Remove deprecated option automatic introduction. | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |