aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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.
2020-07-09Add test for #10890 derive vs abstractGaëtan Gilbert
2020-07-09Overlay for removing struc_tupleGaëtan Gilbert
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
This requires updating the parameter count at section end, I felt it was easier to do with rebuild_function but it could be done in discharge if needed. Incidentally fixes #12649.
2020-07-09Merge PR #11836: [obligations] Functionalize Program stateGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive ↵Enrico Tassi
projection Reviewed-by: ejgallego Ack-by: gares
2020-07-08declare: Add [save_regular] API for obligation-ignoring proofsGaëtan Gilbert
2020-07-08[ci] Overlay for metacoq and rewriterEmilio Jesus Gallego Arias
2020-07-08[declare] Allow obligations update on equations closing hook.Emilio Jesus Gallego Arias
This is also needed in equations.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:04:51 +0000