aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-22Preparing to simplifying the structure of type "tolerability".Hugo Herbelin
The "Any" case was not reached formerly for ETPattern and ETConstr as far as I can see. So there should be no change of semantics.
2020-02-21Merge PR #11617: [init] Add `-boot` option to avoid binding `Coq.` prefix.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: herbelin
2020-02-21Merge PR #11648: [test-suite] Fix output tests due to merge problems.Hugo Herbelin
Reviewed-by: herbelin
2020-02-20[test-suite] Fix output tests due to merge problems.Emilio Jesus Gallego Arias
2020-02-20Merge PR #11143: In Print/Check/Show, adopt the view that the attached type ↵Emilio Jesus Gallego Arias
information may impact the display of coercion and implicit arguments. Reviewed-by: ejgallego
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding ↵Emilio Jesus Gallego Arias
notation format + new notion of format associated to a given interpretation Ack-by: maximedenes
2020-02-20[init] Add `-boot` option to avoid binding `Coq.` prefix.Emilio Jesus Gallego Arias
This is useful when we want to have finer control of the location of files in the bootstrap process, for example when building using Dune. Also, this makes options consistent with what `coqdep` already uses for bootstrap. The main use case for `-boot` is to replace the hardcoded `add_load_path (coqlib () / theories)` with `-R dir Coq`, where dir is controlled by the build system. In particular, we use `-R . Coq` as we `cd` into the directory the package is, so without boot we'd have to hardcode the `theories` path in Dune itself. which seems less robust. Notably after this change the only part of the build that uses `coqlib` is the micromega solver, but that can be tweaked so if coqlib is not set it will use the one in the path. IMO not having to set "coqlib" is a good property if we want a more compositional setup.
2020-02-21Merge PR #11329: Fixing #11114: anomaly with Extraction Implicit on records.Kazuhiko Sakaguchi
Reviewed-by: pi8027
2020-02-20Merge PR #11616: [coqdep] Tweak changelog after recent PRs.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2020-02-20Merge PR #11633: Add doc/unreleased.rst to .gitignore.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-20Merge PR #11630: [make] Fix makefile variable after plugin .v files moveGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2020-02-20Merge PR #11612: CoqIDE: allow opening multiple files at onceHugo Herbelin
2020-02-20Adding changelog.Hugo Herbelin
2020-02-20Fixing #11114 (anomaly with Extraction Implicit on records).Hugo Herbelin
This was due to an inconsistency in handling implicit arguments in the fields and in the constructor of a record.
2020-02-19Merge PR #11499: Clarify expectations for overlay creationEmilio Jesus Gallego Arias
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-02-19Merge PR #11302: Add --fuzz, --real, --user to timing scriptsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: jfehrle
2020-02-19Merge PR #11636: Revert buggy commit mistakenly pushed with #11530Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ↵Hugo Herbelin
entries)." This reverts commit 29919b725262dca76708192bde65ce82860747be. It was pushed by mistake as part of #11530. Sorry about it.
2020-02-19Overlays for Equations, QuickChick and Iris.Hugo Herbelin
2020-02-19Adding change log for #10832.Hugo Herbelin
2020-02-19Short allusion in refman on the existence of a generic and specific format.Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format.
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-19Choosing a standard format for the "rew dependent" notation.Hugo Herbelin
2020-02-19Preparing fix to #6082 and #7766: Renaming type scope_elem and its elements.Hugo Herbelin
This is in anticipation of defining a new type type specific_notation = LastLonelyNotation | NotationInScope
2020-02-19Add doc/unreleased.rst to .gitignore.Théo Zimmermann
And remove outdated entries on tutorials.
2020-02-19[make] Fix makefile variable after plugin .v files moveEmilio Jesus Gallego Arias
This is a bug due to #11529
2020-02-18Merge PR #11530: Fixes custom entries precedence bugs (#11331 part)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: mattam82
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
Reviewed-by: anton-trunov
2020-02-17[coqdep] Tweak changelog after recent PRs.Emilio Jesus Gallego Arias
2020-02-17Merge PR #11593: Update bug report address in coqwc man page.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-17Merge PR #11614: Show apostrophes and backticks in HTML doc, too.Théo Zimmermann
Reviewed-by: Zimmi48
2020-02-17Merge PR #11589: [coqdep] Remove support for `-c` ocamldep replacement.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
to control uniform parameters. This replaces the attribute.
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
2020-02-16Show apostrophes and backticks in HTML, too.Jim Fehrle
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
This reverts commit 03c48bb6943312e606b80b7af65b1ccb7122a386.
2020-02-16Suite picking numeral notationHugo Herbelin
Ceci est une suite à numeral notation in custom entries, cherchant à raffiner la compatibilité entre entrées. C'est mélangé avec le "pick" précédent, et c'est en chantier.
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-16Adding change log.Hugo Herbelin
2020-02-16Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).Hugo Herbelin
This fixes also #9640 part 1.
2020-02-16Mini-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-16Custom 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-16CoqIDE: allow opening multiple files at onceErika
2020-02-15Reusing type production_level for the result of adjust_level.Hugo Herbelin
2020-02-15Reorganize 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-15Dead code in Egramcoq.adjust_level.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:03:15 +0000