aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-07-23Hint Opaque/Transparent/Unfold: don't error on opaque constantsGaëtan Gilbert
Helps with #12566
2020-07-23Merge PR #12672: Fix failing macOS build.Gaëtan Gilbert
Ack-by: JasonGross Reviewed-by: SkySkimmer
2020-07-23Ignore installation failure during call to brew.Théo Zimmermann
Note that all the packages that we request are correctly installed and the observed failure is independent (related to ruby which is not a direct nor indirect dependency, only a dependency of brew itself). The generated CoqIDE package has been tested and works correctly (with no missing icon).
2020-07-23Merge PR #12679: Remove redundant data from VM case switch.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: silene
2020-07-23Merge PR #12698: Fixing mention of `unfold` as example of tactic taking a ↵Théo Zimmermann
qualid in tactic notations Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-07-22Merge PR #12715: Add Coqtail to CIGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-22Merge PR #12664: Turn various anomalies into regular errors in primitive ↵Pierre-Marie Pédrot
declaration path Reviewed-by: ppedrot
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
No need to store the case_info, all the data is reconstructible from the context. Furthermore, this reconstruction is performed in a context where we already access the environment, so performance is not at stake. Hopefully this will also reduce the number of globally allocated VM values, since the switch representation now only depends on the shape of the inductive type.
2020-07-21Merge PR #12714: [declare] Remove some dead code in declare_mutual_definitionGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-07-21Add Coqtail to CIwhonore
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-21Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a ↵Emilio Jesus Gallego Arias
generic printing format in anticipation of further not-only-parsing uses of the notation Reviewed-by: ppedrot
2020-07-20[declare] Remove some dead code in declare_mutual_definitionEmilio Jesus Gallego Arias
This is a leftover after the unification of constant information, `kind` is now correctly set by the single caller of `Obls.add_mutual_definitions`.
2020-07-20Merge PR #12712: CI: deploy make-built stdlib docEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-20Merge PR #12660: Fix typo in contributing guide.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-20CI: deploy make-built stdlib docGaëtan Gilbert
Workaround #12699 Alternative to #12700
2020-07-20Merge PR #12684: Do not print constructor and inductive types as terms when ↵Gaëtan Gilbert
asked to be printed as themselves Reviewed-by: SkySkimmer
2020-07-19Merge PR #12680: Better location for match! pattern variables in Ltac2.Kenji Maillard
Reviewed-by: kyoDralliam
2020-07-18Clarify the Ltac2 invalid identifier message.Pierre-Marie Pédrot
2020-07-18Better location for match! pattern variables in Ltac2.Pierre-Marie Pédrot
2020-07-18Merge PR #12588: [exn] Remove some uses of printPierre-Marie Pédrot
Ack-by: gares Reviewed-by: ppedrot
2020-07-18Merge PR #12696: [gramlib] Remove legacy located exception wrapper in favor ↵Pierre-Marie Pédrot
of standard infrastructure. Reviewed-by: ppedrot
2020-07-18Merge PR #12708: Do not store the full environment inside ssr ast_closure_term.Enrico Tassi
Reviewed-by: gares
2020-07-17Add a changelog.Pierre-Marie Pédrot
2020-07-17Do not store the full environment inside ssr ast_closure_term.Pierre-Marie Pédrot
Apart from being verboten to marshal Environ.env, this should use much less memory on-disk. Fixes #12707.
2020-07-17Documenting new primitive entry evaluable_ref usable for tactic notations.Hugo Herbelin
2020-07-17Add tests for the interpretation of "unfold".Hugo Herbelin
2020-07-17Merge PR #12693: [search] Don't use ad-hoc Dumpglob table for SearchHugo Herbelin
Reviewed-by: herbelin
2020-07-17Merge PR #12670: Advertise switch to maintainer teams and credit maintainers.Emilio Jesus Gallego Arias
Reviewed-by: jfehrle
2020-07-17Merge PR #12701: CI: Use bundled compcert for VSTEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-17Merge PR #12702: CI: pass -silent to coqchk in compcert jobEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-17Merge PR #12683: Fixes #12682: printing bug with recursive notations for ↵Emilio Jesus Gallego Arias
n-ary applications used with applied references Reviewed-by: ejgallego
2020-07-17Merge PR #12631: Fix record pattern interpretation with implicit argumentsEmilio Jesus Gallego Arias
Reviewed-by: herbelin
2020-07-17Wording improvements.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-07-17CI: pass -silent to coqchk in compcert jobGaëtan Gilbert
Otherwise gitlab stops logging somewhere in the middle. Also pass -o because we can.
2020-07-17CI: Use bundled compcert for VSTGaëtan Gilbert
2020-07-16[gramlib] Remove legacy located exception wrapper in favor of standard ↵Emilio Jesus Gallego Arias
infrastructure. The old wrapper was basically unused, this PR also fixes backtraces in some class of bugs such as https://github.com/coq/coq/issues/12695
2020-07-16Merge PR #12677: Fix #12513: coq no longer reports mismatched version numbers.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: gares
2020-07-16Merge PR #12675: Don't catch anomalies for evarconv "cannot find an ↵Emilio Jesus Gallego Arias
instance" error Reviewed-by: ejgallego
2020-07-15Do not print global refs as terms when asked to be printed as themselves.Hugo Herbelin
This was already the case for constant, but not for constructors and inductive types. For instance, in message "The constructor @cons (in type list) is expected to ..." we don't want a @ to be printed.
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
This is to anticipate further not-only-parsing uses of the notation.
2020-07-15[search] Don't use ad-hoc Dumpglob table for SearchEmilio Jesus Gallego Arias
This is an alternative to #12663 ; much preferable as the kind information is already stored in the constant object.
2020-07-15Merge PR #12671: Minor improvement to CI logsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-15Merge PR #12673: Fix fiat_crypto(_ocaml) needs/dependenciesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-15Merge PR #12692: Compatibility of make-change-log with MacOS X whose "sed" ↵Emilio Jesus Gallego Arias
does not support the "\+" operator of regular expressions Reviewed-by: ejgallego
2020-07-15Compatibility of make-change-log with MacOS X whose "sed" does not support "\+".Hugo Herbelin
We make it compatible by expanding "[0-9]\+" into "[0-9][0-9]*".
2020-07-13Advertise switch to maintainer teams and credit maintainers.Théo Zimmermann
2020-07-13Merge PR #12681: tactics.rst: `Require A` is enough for `A`'s hintsThéo Zimmermann
Reviewed-by: Zimmi48
2020-07-13Don't catch anomalies for evarconv "cannot find an instance" errorGaëtan Gilbert
2020-07-12Adding change log.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:37:05 +0000