aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Correct some spelling errorsmasterGravatar Benjamin Barenblat2018-07-22
| | | | | | | | | | Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
* Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.Gravatar Enrico Tassi2018-07-20
|\
* \ Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.Gravatar Enrico Tassi2018-07-20
|\ \
* \ \ Merge PR #7941: Extend QuestionMark to produce a better error message in ↵Gravatar Pierre-Marie Pédrot2018-07-19
|\ \ \ | | | | | | | | | | | | case of missing record field
| | * | Remove declare_object for SsrHave NoTCResolution.Gravatar Maxime Dénès2018-07-19
| |/ / |/| | | | | | | | | | | | | | | | | 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.
* | | Merge PR #8054: [dev] Autogenerate OCaml dev files.Gravatar Enrico Tassi2018-07-18
|\ \ \
* \ \ \ Merge PR #7897: Remove fourier pluginGravatar Enrico Tassi2018-07-18
|\ \ \ \
* \ \ \ \ Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence`Gravatar Enrico Tassi2018-07-18
|\ \ \ \ \
| | * | | | Remove fourier pluginGravatar Maxime Dénès2018-07-17
| |/ / / / |/| | | | | | | | | | | | | | As stated in the manual, the fourier tactic is subsumed by lra.
| | | * | Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | [build] Build Coq and plugins with `-strict-sequence`Gravatar Emilio Jesus Gallego Arias2018-07-14
| | | | | | | | | | | | | | | | | | | | Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins.
* | | | [ltac] Remove unused functions / constructors.Gravatar Emilio Jesus Gallego Arias2018-07-14
|/ / / | | | | | | | | | Catched by compiling the ml files from ml4.
| * | [dev] Autogenerate OCaml dev files.Gravatar Emilio Jesus Gallego Arias2018-07-12
| | | | | | | | | | | | | | | | | | | | | | | | 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
* | | Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.".
| * Export a function to apply toplevel tactic values in Tacinterp.Gravatar Pierre-Marie Pédrot2018-07-10
| | | | | | | | | | This is a function that keeps beeing asked or reimplemented. It doesn't hurt adding it to the Ltac API.
* | Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
|/ | | | | | | | | | 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.
* refine: obey the use_unification_heuristics flagGravatar Matthieu Sozeau2018-07-05
|
* Merge PR #7746: Many small cleanups removing unused arguments and functionsGravatar Pierre-Marie Pédrot2018-07-05
|\
* \ Merge PR #7979: TACTIC EXTEND in coqppGravatar Emilio Jesus Gallego Arias2018-07-05
|\ \
| | * Evarutil.(e_)new_Type: remove unused env argumentGravatar Gaëtan Gilbert2018-07-03
| | |
| | * Remove unused env argument to fresh_sort_in_familyGravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | (Universes and Evd)
| | * Coq_omega: remove unused Goal.entersGravatar Gaëtan Gilbert2018-07-03
| | | | | | | | | | | | Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
| | * Remove unused function Coq_omega.timing.Gravatar Gaëtan Gilbert2018-07-03
| | |
| | * Taccoerce: remove various unused arguments.Gravatar Gaëtan Gilbert2018-07-03
| | |
| | * Pptactic: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
| |/ |/|
* | Merge PR #7703: Add an option to force parameters to be uniformGravatar Matthieu Sozeau2018-07-02
|\ \
| | * Remove the hardcoded compatibility wit_hyp -> wit_var from the parser.Gravatar Pierre-Marie Pédrot2018-07-02
| | |
| | * Slight simplification of the Tacentries API to register ML tactics.Gravatar Pierre-Marie Pédrot2018-07-02
| | | | | | | | | | | | It was forcing the macro to generate code that was useless.
| | * Moving various ml4 files to mlg.Gravatar Pierre-Marie Pédrot2018-07-02
| |/ |/|
* | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ \ | | | | | | | | | points of Camlp5
| | * Implement uniform parameters in ComInductiveGravatar Jasper Hugunin2018-07-01
| |/ |/| | | | | Don't allow notations attached to uniform inductives
* | Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ | | | | | | | | | Z into three files
* | | Split the Ssrmatching module between code and grammar rules.Gravatar Pierre-Marie Pédrot2018-06-30
| | | | | | | | | | | | Fixes #7857.
| | * Port g_tactic to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | |
| | * Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
| |/ |/| | | | | | | | | | | | | | | 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.
| * Splitting primitive numeral parser/printer for positive, N, Z into three files.Gravatar Hugo Herbelin2018-06-29
| |
* | Merge PR #7890: Inline a function from Quote used in setoid_ring.Gravatar Maxime Dénès2018-06-29
|\ \ | |/ |/|
* | Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\ \
* \ \ Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Gravatar Pierre-Marie Pédrot2018-06-26
|\ \ \ | | | | | | | | | | | | constants
| | * | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |/ / |/| |
| * | universes_of_constr don't include universes of monomorphic constantsGravatar Gaëtan Gilbert2018-06-26
| | | | | | | | | | | | | | | Apparently it was not useful. I don't remember what I was thinking when I added it.
* | | Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorGravatar Maxime Dénès2018-06-25
|\ \ \
* \ \ \ Merge PR #7236: [ssr] simpler semantics for delayed clearsGravatar Maxime Dénès2018-06-23
|\ \ \ \
* | | | | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | | | | | | | | | | | | | | | | This brings more compatibility with handling of mutual primitive records in the kernel.
* | | | | Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | | | | | | | | | | | | | | | | This is a first step towards the acceptance of mutual record types in the kernel.
| * | | | [ssr] implement {}/v as a short hand for {v}/v when v is an idGravatar Enrico Tassi2018-06-22
| | | | |
| * | | | [ssr] simplify delayed clearsGravatar Enrico Tassi2018-06-22
| | |/ / | |/| | | | | | | | | | | | | | - we always rename - we compile {clear}/view to /view{clear}
* | | | [ssr] matching: use eq_constr_nounivs in approximated matchingGravatar Enrico Tassi2018-06-22
| | | |
* | | | [ssr] set: merge universe constraints before type checking the termGravatar Enrico Tassi2018-06-22
|/ / /
| | * Further cleanup: do not export the closed_term Ltac entry.Gravatar Pierre-Marie Pédrot2018-06-21
| | | | | | | | | | | | | | | We only use it locally, so we simply register the ML tactic inside the module but we do not export the syntax.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 13:57:47 +0000