| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-11-03 | Merge PR #8745: Fixes #3468: making tactic-in-term sensitive to ↵ | Pierre-Marie Pédrot | |
| interpretation scopes | |||
| 2018-11-03 | Merge PR #8844: Move abstract out of tactics.ml | Pierre-Marie Pédrot | |
| 2018-11-02 | coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax | Gaëtan Gilbert | |
| I think for instance the new code in this diff is cleaner and more systematic: ~~~diff VERNAC COMMAND EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { +| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater } -> { - let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } END ~~~ | |||
| 2018-11-02 | Simplify use of polymorphism/program globals in attributes | Gaëtan Gilbert | |
| 2018-11-02 | rewrite: attributes handle is_univ_poly, is_program_mode | Gaëtan Gilbert | |
| 2018-11-02 | Remove is_universe_polymorphism in funind | Gaëtan Gilbert | |
| Funind doesn't support polymorphism. | |||
| 2018-11-02 | Command driven attributes. | Gaëtan Gilbert | |
| Commands need to request the attributes they use, with the API encouraging them to error on unsupported attributes. | |||
| 2018-11-02 | Move attributes out of vernacinterp to new attributes module | Gaëtan Gilbert | |
| 2018-10-31 | Fixes rest of #3468 (tactic-in-term was not respecting scopes). | Hugo Herbelin | |
| We do it by passing interning env to ltac interning. Collecting scopes was already done by side-effect internally to Constrintern. We expose the side-effect to ltac. | |||
| 2018-10-31 | Clarify meaning of boolean in IPatDispatch | Maxime Dénès | |
| 2018-10-31 | [ssr] better doc for the IPatDispatch AST | Enrico Tassi | |
| 2018-10-31 | [ssr] use tclDISPATCH for IPatDispatch (fix #8544) | Enrico Tassi | |
| 2018-10-31 | Merge PR #8759: Fix #8755: Uncaught exception ↵ | Hugo Herbelin | |
| Ltac_plugin.Taccoerce.CannotCoerceTo. | |||
| 2018-10-31 | Merge PR #8864: Avoid passing empty environments | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |