aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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
2020-02-15Fixing 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-15Fixes #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-14Merge pull request #11605 from ppedrot/ltac2-annotate-match-branchKenji Maillard
Annotate Ltac2 match macro variables with their type.
2020-02-14Merge PR #11557: Use thunks to univ instead of lazy constr for template typingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-14Apply suggestions from code reviewJason Gross
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-02-14Annotate 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-14Merge PR #11599: Spell out index entry suffixes in main index, e.g. ↵Théo Zimmermann
"(tactic)" instead of "(tacn)" Reviewed-by: Zimmi48
2020-02-14Merge PR #11468: [doc] fix typo & update release-process.md for opam/docker ↵Théo Zimmermann
packaging Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-02-14Overlay for Inductive.type_of_inductive doesn't take an envGaëtan Gilbert
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-14Merge 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-13Spell out the entry suffix in the main indexJim 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:39:18 +0000