| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-01-24 | Merge PR #9269: Move and rewrite intro pattern section | Théo Zimmermann | |
| Ack-by: Zimmi48 Ack-by: anton-trunov Ack-by: jfehrle | |||
| 2019-01-23 | Move and rewrite documentation for intro patterns that was under | Jim Fehrle | |
| the intros tactic to its own subsection. Add grammar and examples. | |||
| 2019-01-22 | Make `Add Morphism` not rely on Refine Instance | Maxime Dénès | |
| 2018-12-22 | Merge PR #9248: Fix #7904: update proofview env after ltac constr:() | Pierre-Marie Pédrot | |
| 2018-12-19 | Fix #7904: update proofview env after ltac constr:() | Gaëtan Gilbert | |
| (in case of side effects) Also: Fix #4781 Fix #4496 | |||
| 2018-12-19 | Merge PR #9139: [engine] Allow debug printers to access the environment. | Pierre-Marie Pédrot | |
| 2018-12-17 | Merge PR #9153: [api] Move reduction modules to `tactics` | Pierre-Marie Pédrot | |
| 2018-12-14 | [proof] Rework proof interface. | Emilio Jesus Gallego Arias | |
| - deprecate the old 5-tuple accessor in favor of a view record, - move `name` and `kind` proof data from `Proof_global` to `Proof`, this will prove useful in subsequent functionalizations of the interface, in particular this is what abstract, which lives in the monads, needs in order no to access global state. - Note that `Proof.t` and `Proof_global.t` are redundant anyways. | |||
| 2018-12-13 | [engine] Allow debug printers to access the environment. | Emilio Jesus Gallego Arias | |
| This should improve correctness and will be needed for the PRs that remove global access to the proof state. | |||
| 2018-12-12 | Higher-level libobject API for objects with fixed scopes | Maxime Dénès | |
| 2018-12-11 | [api] Move reduction modules to `tactics` | Emilio Jesus Gallego Arias | |
| These modules do actually belong there. We have to slightly reorganize printers, removing a couple of duplicated ones in the way. | |||
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 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-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-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 | 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 #7925: Clean transparent state | Maxime Dénès | |
| 2018-11-19 | Merge PR #9003: [vernacextend] Consolidate extension points API | 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 | [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 the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 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 | Fix #4771: Substitution of inline global reference in tactics is broken | 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 | 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 | 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 | |
| 2018-10-30 | Generalizing the various evar_map printers in Termops over an environment. | Hugo Herbelin | |
| This is a step towards limiting calls to the global environment. Incidentally unify naming evd -> sigma in Termops. | |||
| 2018-10-30 | Remove fully_empty_glob_sign which uses a dummy environment | Maxime Dénès | |
| 2018-10-30 | Distinguish globalization and pretyping error on unbound variable | Maxime Dénès | |
| We can then avoid passing an empty env. | |||
| 2018-10-30 | Move abstract out of tactics.ml | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |