aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-20Unconditionally print explanation for universe inconsistenciesGaëtan Gilbert
ie regardless of the Print Universes flag. AFAICT there is no point in skipping them.
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-20Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-20Adding a printer for GlobEnv in ocamldebug.Hugo Herbelin
2020-02-19Update copyright in refman to year 2020.Théo Zimmermann
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-19Remove the dependency in float.cmo and uint63.cmo for building votour.Hugo Herbelin
This was useless since PR #11247 and is a cause of failure in bytecode compilation on some exotic architectures (such as "armel").
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-19Fix #11549: Ltac2 is incompatible with $.Pierre-Marie Pédrot
We use the same kind of trick as the one we used for &IDENT, namely check that no space appear between the dollar sign and the identifier.
2020-02-19Fix #11552: Ltac2 breaks query commands during proofs.Pierre-Marie Pédrot
Actually, callers of the Pvernac.register_proof_mode function have to manually register the parsing of vernacular queries themselves. This probably qualifies as an oversight from myself.
2020-02-19ComInductive: use lbound=Prop iff non polymorphicGaëtan Gilbert
This avoids having to interp params and intern arities twice.
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-18Deprecate unsafe_type_ofGaëtan Gilbert
2020-02-18Merge PR #10204: Remove `unsafe_type_of` from `Coercion`Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: mattam82
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-02-17Take "Implicit Types" into account when printing terms.Hugo Herbelin
2020-02-17Merge PR #11350: stdlib List: add [remove'] and [count_occ'] that use [filter]Hugo Herbelin
Reviewed-by: anton-trunov
2020-02-17Mini-improvements in when to skip coercions or explicitly print implicit args.Hugo Herbelin
If a return type is given to a match/if/let, then we are in context (and thus may skip coercions or not make explicit those implicit arguments inferable from context). Note that the notion of "inferable from context" remains anyway an approximation in the case of implicit arguments. The body of a fix/cofix is also in context. Also fixed an inconsistency with parsing in the scope used to print the body of a fix.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 00:33:35 +0000