| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-22 | Fix #8251: remove "the the" occurrences | Gaëtan Gilbert | |
| 2018-07-29 | Adding support for custom entries in notations. | Hugo Herbelin | |
| - New command "Declare Custom Entry bar". - Entries can have levels. - Printing is done using a notion of coercion between grammar entries. This typically corresponds to rules of the form 'Notation "[ x ]" := x (x custom myconstr).' but also 'Notation "{ x }" := x (in custom myconstr, x constr).'. - Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).' are natively recognized. - Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).' are natively recognized. Incidentally merging ETConstr and ETConstrAsBinder. Noticed in passing that parsing binder as custom was not done as in constr. Probably some fine-tuning still to do (priority of notations, interactions between scopes and entries, ...). To be tested live further. | |||
| 2018-07-26 | Replace iter + ref by fold_left | Maxime Dénès | |
| 2018-07-26 | Coercions cleanup: use GlobRef.t instead of constr | Maxime Dénès | |
| 2018-07-26 | Merge PR #8050: Cleanup VERNAC EXTEND | Maxime Dénès | |
| 2018-07-25 | Merge PR #8139: Replace all the CoInductives with Variants in the SSR plugin | Enrico Tassi | |
| 2018-07-25 | Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2) | Hugo Herbelin | |
| 2018-07-25 | Replace all the CoInductives with Variants in the SSR plugin | Kazuhiko Sakaguchi | |
| 2018-07-24 | Projections use index representation | Gaëtan Gilbert | |
| The upper layers still need a mapping constant -> projection, which is provided by Recordops. | |||
| 2018-07-20 | Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp. | Enrico Tassi | |
| 2018-07-20 | Merge PR #8089: Remove declare_object for SsrHave NoTCResolution. | Enrico Tassi | |
| 2018-07-19 | Merge PR #7941: Extend QuestionMark to produce a better error message in ↵ | Pierre-Marie Pédrot | |
| case of missing record field | |||
| 2018-07-19 | Remove 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-18 | Merge PR #8054: [dev] Autogenerate OCaml dev files. | Enrico Tassi | |
| 2018-07-18 | Merge PR #7897: Remove fourier plugin | Enrico Tassi | |
| 2018-07-18 | Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence` | Enrico Tassi | |
| 2018-07-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-07-17 | Change 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-16 | Add Extract Inlined Constant directives for {String,Ascii}.eqb | Jason Gross | |
| 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-12 | Statically typecheck the VERNAC EXTEND wrapper. | Pierre-Marie Pédrot | |
| This moves the typing code from the macro expansion to the extension registering mechanism, bringing in more static safety. We also seize the opportunity to remove dead code in the macro. | |||
| 2018-07-12 | Tactic deprecation machinery | Maxime 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-10 | Export 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-07 | Introduce 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-05 | refine: obey the use_unification_heuristics flag | Matthieu Sozeau | |
| 2018-07-05 | Merge PR #7746: Many small cleanups removing unused arguments and functions | Pierre-Marie Pédrot | |
| 2018-07-05 | Merge PR #7979: TACTIC EXTEND in coqpp | Emilio Jesus Gallego Arias | |
| 2018-07-03 | Evarutil.(e_)new_Type: remove unused env argument | Gaëtan Gilbert | |
| 2018-07-03 | Remove unused env argument to fresh_sort_in_family | Gaëtan Gilbert | |
| (Universes and Evd) | |||
| 2018-07-03 | Coq_omega: remove unused Goal.enters | Gaëtan Gilbert | |
| Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3. | |||
| 2018-07-03 | Remove unused function Coq_omega.timing. | Gaëtan Gilbert | |
| 2018-07-03 | Taccoerce: remove various unused arguments. | Gaëtan Gilbert | |
| 2018-07-03 | Pptactic: remove unused arguments | Gaëtan Gilbert | |
| 2018-07-02 | Merge PR #7703: Add an option to force parameters to be uniform | Matthieu Sozeau | |
| 2018-07-02 | Remove the hardcoded compatibility wit_hyp -> wit_var from the parser. | Pierre-Marie Pédrot | |
| 2018-07-02 | Slight 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-02 | Moving various ml4 files to mlg. | Pierre-Marie Pédrot | |
| 2018-07-02 | Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵ | Emilio Jesus Gallego Arias | |
| points of Camlp5 | |||
| 2018-07-01 | Implement uniform parameters in ComInductive | Jasper Hugunin | |
| Don't allow notations attached to uniform inductives | |||
| 2018-07-01 | Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵ | Emilio Jesus Gallego Arias | |
| Z into three files | |||
| 2018-06-30 | Split the Ssrmatching module between code and grammar rules. | Pierre-Marie Pédrot | |
| Fixes #7857. | |||
| 2018-06-29 | Port g_tactic to the homebrew GEXTEND parser. | Pierre-Marie Pédrot | |
| 2018-06-29 | Use 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-29 | Splitting primitive numeral parser/printer for positive, N, Z into three files. | Hugo Herbelin | |
| 2018-06-29 | Merge PR #7890: Inline a function from Quote used in setoid_ring. | Maxime Dénès | |
| 2018-06-27 | Merge PR #7863: Remove Sorts.contents | Pierre-Marie Pédrot | |
| 2018-06-26 | Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵ | Pierre-Marie Pédrot | |
| constants | |||
| 2018-06-26 | Remove Sorts.contents | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |