aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-17Remove automatic formatting of ComHints.Pierre-Marie Pédrot
This is about the third time I try to kill this file but for some reason it is still here.
2020-07-17Add changelog.Pierre-Marie Pédrot
2020-07-17Tweak the warning for arbitrary term hints.Pierre-Marie Pédrot
Fixes #11970.
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
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
A special case for recursive n-ary applications was missing when the head of the application was a reference.
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
As the text says later: > Hints should only be made available when the module they are defined in is imported, not just required.
2020-07-11Merge PR #12650: Recordops: unify struc_typ summary record and libobject ↵Pierre-Marie Pédrot
entry struc_tuple Reviewed-by: ppedrot
2020-07-11Merge PR #12646: Correctly readback blocked CaseInvert matches in VM/nativePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-11Merge PR #12635: Correct comment and clarify constantPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-07-10Merge PR #12638: Some changes of representation in TacredEnrico Tassi
Ack-by: backtracking Reviewed-by: gares
2020-07-10Add changelog.Pierre-Marie Pédrot
2020-07-10Fix #12513: coq no longer reports mismatched version numbers.Pierre-Marie Pédrot
2020-07-10Minor improvement to CI logsGaëtan Gilbert
- don't `set -x` while loading overlays, non-verbose untaring - ls _build_ci to help figure out artifact download issues
2020-07-10Merge PR #12666: Add test for #10890 derive vs abstractEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-10Fix fiat_crypto(_ocaml) needs/dependenciesGaëtan Gilbert
It seems gitlab has issues with missing transitive dependencies, for instance in https://gitlab.com/coq/coq/-/pipelines/164834444 rewriter failed (missing overlay), fiat_crypto was skipped and fiat_crypto_ocaml was incorrectly started and so failed. May also fix (intermittent?) issue where it doesn't download the rewriter or bignum artifact and gets incompatible ocaml when compiling.
2020-07-10Merge PR #12537: Take into account the existing delta-resolver when starting ↵Gaëtan Gilbert
a new interactive module or module type Reviewed-by: SkySkimmer
2020-07-09Merge PR #12542: Defined arbitrary base logarithms (Rlog) and added natural ↵Michael Soegtrop
lemmas to the Real library Reviewed-by: MSoegtropIMC Ack-by: silene
2020-07-09[error handling] Anomaly in Conversion is a "precatchable_exception"Emilio Jesus Gallego Arias
This is just a fixup, likely all the places that are matching on `UserErr` directly are just buggy.
2020-07-09[reductionops] Comment about absorption of anomalies.Emilio Jesus Gallego Arias
Co-authored-by: <Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
2020-07-09[exn] Remove some uses of printEmilio Jesus Gallego Arias
Exceptions should not printed except for the top-level. There is the weird anomaly-absorbing code in `Reductionops`, I wonder how frequent that case is, but as the exception is absorbed printing there could have a real impact.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 01:39:34 +0000