aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2018-07-20Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Enrico Tassi
2018-07-20Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.Enrico Tassi
2018-07-19Merge PR #7941: Extend QuestionMark to produce a better error message in ↵Pierre-Marie Pédrot
case of missing record field
2018-07-19Remove declare_object for SsrHave NoTCResolution.Maxime Dénès
IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like `Global Set SsrHave NoTCResolution`. I don't think it is needed (just let the user write the desired locality), but if it is, the right way of doing it is to let clients of Goptions specify a default locality.
2018-07-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
2018-07-18Merge PR #7897: Remove fourier pluginEnrico Tassi
2018-07-18Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence`Enrico Tassi
2018-07-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields.
2018-07-14[build] Build Coq and plugins with `-strict-sequence`Emilio Jesus Gallego Arias
Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins.
2018-07-14[ltac] Remove unused functions / constructors.Emilio Jesus Gallego Arias
Catched by compiling the ml files from ml4.
2018-07-12[dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias
For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
2018-07-12Tactic deprecation machineryMaxime Dénès
We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
2018-07-10Export a function to apply toplevel tactic values in Tacinterp.Pierre-Marie Pédrot
This is a function that keeps beeing asked or reimplemented. It doesn't hurt adding it to the Ltac API.
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins.
2018-07-05refine: obey the use_unification_heuristics flagMatthieu Sozeau
2018-07-05Merge PR #7746: Many small cleanups removing unused arguments and functionsPierre-Marie Pédrot
2018-07-05Merge PR #7979: TACTIC EXTEND in coqppEmilio Jesus Gallego Arias
2018-07-03Evarutil.(e_)new_Type: remove unused env argumentGaëtan Gilbert
2018-07-03Remove unused env argument to fresh_sort_in_familyGaëtan Gilbert
(Universes and Evd)
2018-07-03Coq_omega: remove unused Goal.entersGaëtan Gilbert
Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
2018-07-03Remove unused function Coq_omega.timing.Gaëtan Gilbert
2018-07-03Taccoerce: remove various unused arguments.Gaëtan Gilbert
2018-07-03Pptactic: remove unused argumentsGaëtan Gilbert
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
2018-07-02Remove the hardcoded compatibility wit_hyp -> wit_var from the parser.Pierre-Marie Pédrot
2018-07-02Slight simplification of the Tacentries API to register ML tactics.Pierre-Marie Pédrot
It was forcing the macro to generate code that was useless.
2018-07-02Moving various ml4 files to mlg.Pierre-Marie Pédrot
2018-07-02Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Emilio Jesus Gallego Arias
points of Camlp5
2018-07-01Implement uniform parameters in ComInductiveJasper Hugunin
Don't allow notations attached to uniform inductives
2018-07-01Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Emilio Jesus Gallego Arias
Z into three files
2018-06-30Split the Ssrmatching module between code and grammar rules.Pierre-Marie Pédrot
Fixes #7857.
2018-06-29Port g_tactic to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Pierre-Marie Pédrot
The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.
2018-06-29Splitting primitive numeral parser/printer for positive, N, Z into three files.Hugo Herbelin
2018-06-29Merge PR #7890: Inline a function from Quote used in setoid_ring.Maxime Dénès
2018-06-27Merge PR #7863: Remove Sorts.contentsPierre-Marie Pédrot
2018-06-26Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Pierre-Marie Pédrot
constants
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
Apparently it was not useful. I don't remember what I was thinking when I added it.
2018-06-25Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorMaxime Dénès
2018-06-23Merge PR #7236: [ssr] simpler semantics for delayed clearsMaxime Dénès
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
This brings more compatibility with handling of mutual primitive records in the kernel.
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
This is a first step towards the acceptance of mutual record types in the kernel.
2018-06-22[ssr] implement {}/v as a short hand for {v}/v when v is an idEnrico Tassi
2018-06-22[ssr] simplify delayed clearsEnrico Tassi
- we always rename - we compile {clear}/view to /view{clear}
2018-06-22[ssr] matching: use eq_constr_nounivs in approximated matchingEnrico Tassi
2018-06-22[ssr] set: merge universe constraints before type checking the termEnrico Tassi
2018-06-21Further cleanup: do not export the closed_term Ltac entry.Pierre-Marie Pédrot
We only use it locally, so we simply register the ML tactic inside the module but we do not export the syntax.
2018-06-21Inline a function from Quote used in setoid_ring.Pierre-Marie Pédrot
The code was wrong as it relies once again on term equality and fails on polymorphic constants. Quote is bound to disappear, so we write a correct version of this 10-line function in setoid_ring.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 05:10:29 +0000