| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-02-16 | Granting #9516 and #9518 (support for numerals and strings in custom entries). | Hugo Herbelin | |
| 2020-02-16 | Adding change log. | Hugo Herbelin | |
| 2020-02-16 | Fixing bug #9521 (anomaly due to missing declaration of level in custom entry). | Hugo Herbelin | |
| This fixes also #9640 part 1. | |||
| 2020-02-16 | Mini-factorization in vernac grammar. | Hugo Herbelin | |
| Unfortunately, we cannot factorize further | x = IDENT; "at"; lev = level; b = OPT constr_as_binder_kind | x = IDENT; b = constr_as_binder_kind without losing the rule | x = IDENT; typ = syntax_extension_type | |||
| 2020-02-16 | Custom entries: accept that no level is mentioned for a subentry. | Hugo Herbelin | |
| If it is for an internal non-terminal then: - if for a subentry different from constr, it refers to the head of the subentry - if in constr, it is 200 by convention If it is on the border of a rule, then: - if it is in a subentry different from the entry it lives, it refers to the head of the subentry (or 200 by convention if in constr) - if it is in the same entry, the rule for associativity tells if a SELF, a NEXT, or (if on the right) a LEVEL | |||
| 2020-02-16 | CoqIDE: allow opening multiple files at once | Erika | |
| 2020-02-15 | Reusing type production_level for the result of adjust_level. | Hugo Herbelin | |
| 2020-02-15 | Reorganize type "production_level" along a more intuitive structure. | Hugo Herbelin | |
| NextLevel = at next level NumLevel n = at level n DefaultLevel = <no mention of level> | |||
| 2020-02-15 | Dead code in Egramcoq.adjust_level. | Hugo Herbelin | |
| 2020-02-15 | Fixing a precedence printing bug with custom entries. | Hugo Herbelin | |
| Insertion of coercion to manage precedence of custom entries are treated in constrextern.ml, while ppconstr.ml is only about the management of precedences for constr. | |||
| 2020-02-15 | Fixes #11331 (unexpected level collisions between custom entries and constr). | Hugo Herbelin | |
| There was a collision at the time of interpreting subentries (in metasyntax.ml) but also at the time of "optimizing" the entries (in egramcoq.ml). Also fixes #9517, fixes #9519, fixes #9640 (part 3). | |||
| 2020-02-14 | Merge pull request #11605 from ppedrot/ltac2-annotate-match-branch | Kenji Maillard | |
| Annotate Ltac2 match macro variables with their type. | |||
| 2020-02-14 | Merge PR #11557: Use thunks to univ instead of lazy constr for template typing | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-02-14 | Apply suggestions from code review | Jason Gross | |
| Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2020-02-14 | test for x[i] notation not breaking Ltac parsing | Andres Erbsen | |
| 2020-02-14 | Annotate Ltac2 match macro variables with their type. | Pierre-Marie Pédrot | |
| This prevents some warnings to be dropped when the variables are not used at the right type. See #11603 for a motivation. | |||
| 2020-02-14 | Merge PR #11599: Spell out index entry suffixes in main index, e.g. ↵ | Théo Zimmermann | |
| "(tactic)" instead of "(tacn)" Reviewed-by: Zimmi48 | |||
| 2020-02-14 | Merge PR #11468: [doc] fix typo & update release-process.md for opam/docker ↵ | Théo Zimmermann | |
| packaging Reviewed-by: Zimmi48 Ack-by: jfehrle | |||
| 2020-02-14 | Overlay for Inductive.type_of_inductive doesn't take an env | Gaëtan Gilbert | |
| 2020-02-14 | Use thunks to univ instead of lazy constr for template typing | Gaëtan Gilbert | |
| 2020-02-14 | Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive ↵ | Maxime Dénès | |
| Parameters) Reviewed-by: Matafou Reviewed-by: Zimmi48 Reviewed-by: maximedenes | |||
| 2020-02-13 | Spell out the entry suffix in the main index | Jim Fehrle | |
| Ex: "(tactic)" instead of "(tacn)" | |||
| 2020-02-13 | [coqdep] Remove support for `-c` ocamldep replacement. | Emilio Jesus Gallego Arias | |
| There is not need for coqdep to ship an `ocamldep` replacement, in particular: - not used in the main build since a long time - not tested - not kept up to date with upstream This allows for a significant reduction of `coqdep` code, including some duplicated code from `ocamllibdep`. `coq_makefile` now uses `ocamllibdep` to process `mllib/mlpack` files, so it has then to be installed. We also remove the residual `-slash` option. | |||
| 2020-02-13 | [coqdep] Merge `-sort` and `-suffix` options. | Emilio Jesus Gallego Arias | |
| They are always used together, no other use case of `-suffix` that I can see. | |||
| 2020-02-13 | Merge PR #11427: Dispatch code ownership of files in dev/doc. | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego Reviewed-by: gares | |||
| 2020-02-13 | Merge PR #11450: Publishing a new version on Zenodo: not a relevant step for ↵ | Emilio Jesus Gallego Arias | |
| beta versions. Reviewed-by: ejgallego | |||
| 2020-02-13 | Merge PR #11441: Add explicit types to changelog entries that were still ↵ | Emilio Jesus Gallego Arias | |
| missing them. Reviewed-by: ejgallego | |||
| 2020-02-13 | [coqinit] Removed unused `with_ml` parameter. | Emilio Jesus Gallego Arias | |
| `theories` now never have `.ml` files inside. | |||
| 2020-02-13 | [build] Consolidate stdlib's .v files under a single directory. | Emilio Jesus Gallego Arias | |
| Currently, `.v` under the `Coq.` prefix are found in both `theories` and `plugins`. Usually these two directories are merged by special loadpath code that allows double-binding of the prefix. This adds some complexity to the build and loadpath system; and in particular, it prevents from handling the `Coq.*` prefix in the simple, `-R theories Coq` standard way. We thus move all `.v` files to theories, leaving `plugins` as an OCaml-only directory, and modify accordingly the loadpath / build infrastructure. Note that in general `plugins/foo/Foo.v` was not self-contained, in the sense that it depended on files in `theories` and files in `theories` depended on it; moreover, Coq saw all these files as belonging to the same namespace so it didn't really care where they lived. This could also imply a performance gain as we now effectively traverse less directories when locating a library. See also discussion in #10003 | |||
| 2020-02-13 | Merge PR #11564: Recognize Default Proof Using in STM | Enrico Tassi | |
| Ack-by: gares | |||
| 2020-02-13 | Merge PR #11417: Move kind_of_type from the kernel to EConstr. | Enrico Tassi | |
| Reviewed-by: SkySkimmer Reviewed-by: gares | |||
| 2020-02-13 | Merge PR #11098: Let Arguments support anonymous implicit arguments | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 Reviewed-by: ejgallego | |||
| 2020-02-13 | Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters) | Gaëtan Gilbert | |
| 2020-02-13 | Delete unused comment | Gaëtan Gilbert | |
| 2020-02-13 | Don't duplicate the inductive keyword for each block elt when parsing | Gaëtan Gilbert | |
| 2020-02-13 | Merge PR #11407: [mltop] Store digest of modules used to compile files. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: maximedenes | |||
| 2020-02-13 | Merge PR #11521: Remove Goptions.opt_name field | Pierre-Marie Pédrot | |
| Reviewed-by: Zimmi48 Reviewed-by: ppedrot | |||
| 2020-02-13 | Update bug report address in coqwc man page. | Gaëtan Gilbert | |
| 2020-02-13 | Merge PR #11457: [toplevel] Refactor control loop | Hugo Herbelin | |
| Ack-by: SkySkimmer Ack-by: gares Reviewed-by: herbelin | |||
| 2020-02-13 | Merge PR #11424: Check instance length in type_of_{inductive,constructor} | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-02-13 | Merge PR #11577: [nix] Fix building of the documentation | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2020-02-13 | Arguments: removing the restriction to set an anonymous parameter implicit. | Hugo Herbelin | |
| This was already possible manually using "{ _ }" in the type of declaration. This was also possible for type classes. So, no reason to forbid in Arguments. | |||
| 2020-02-13 | Implicit arguments: Fixing count of the position in compute_implicit_statuses. | Hugo Herbelin | |
| 2020-02-12 | Merge PR #11582: Split unicoq out of ci-mtac2.sh (keeping 1 CI job) | Emilio Jesus Gallego Arias | |
| Reviewed-by: ejgallego | |||
| 2020-02-12 | Split unicoq out of ci-mtac2.sh (keeping 1 CI job) | Gaëtan Gilbert | |
| No reason to have them in the same .sh | |||
| 2020-02-12 | [toplevel] Make toplevel loop tail-recursive again | Emilio Jesus Gallego Arias | |
| In previous refactorings `vernac_loop` stopped being tail-recursive, we refactor code a bit and make it back into tail-recursive form. | |||
| 2020-02-12 | [toplevel] Refactor control loop | Emilio Jesus Gallego Arias | |
| We refactor control loop a bit to make the code more readable: - the code for unhandled exception is not needed anymore as it cannot happen. - we move the processing of toplevel commands to its own function - we split away diff-specific functions. | |||
| 2020-02-12 | Merge PR #11544: Cleanup some globref related manipulations | Pierre-Marie Pédrot | |
| Reviewed-by: herbelin Reviewed-by: ppedrot | |||
| 2020-02-12 | overlay for removal of optname | Gaëtan Gilbert | |
| 2020-02-12 | Remove Goptions.opt_name field | Gaëtan Gilbert | |
| The standard use is to repeat the option keywords in lowercase, which is basically useless. En passant add doc entry for Dump Arith. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |