aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-14Merge PR #12037: coqdoc: Report location of mismatched '[['Hugo Herbelin
Reviewed-by: herbelin
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: maximedenes Ack-by: ppedrot
2020-04-14Merge PR #11978: Close #11935: section variables do not have universe instances.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-14Merge PR #11985: Fix #11934 equality on constrexpr ignores instances of ↵Pierre-Marie Pédrot
explicit applications Ack-by: herbelin Reviewed-by: ppedrot
2020-04-14Merge PR #12084: [warnings] Be silent about the `set_tag` warning.Pierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-14Merge PR #12054: [ocamlformat] Update to 0.14.0Théo Zimmermann
Reviewed-by: Zimmi48
2020-04-13Merge PR #12089: dune states target: respect user's global verbosity settingEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-04-13[ocamlformat] Update to 0.14.0Emilio Jesus Gallego Arias
No diff to sources (luckily), see release notes at https://discuss.ocaml.org/t/ann-ocamlformat-0-14-0/5435 for more information.
2020-04-13Close #11935: section variables do not have universe instances.Gaëtan Gilbert
2020-04-13Merge PR #11916: [proof] Introduce `prepare_proof` to improve normalization ↵Gaëtan Gilbert
workflow. Reviewed-by: SkySkimmer Ack-by: gares Ack-by: ppedrot
2020-04-13Merge PR #12081: [test-suite] Remove deprecated -I option of coqchk in MakefileGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-13Overlay for partial importsGaëtan Gilbert
2020-04-13Update syntax of Import / Export in documentation.Théo Zimmermann
2020-04-13doc for partial importsGaëtan Gilbert
2020-04-13Partial import inductive(..)Gaëtan Gilbert
NB: 3 dots doesn't play well with PG's sentence detection.
2020-04-13always debug validate failuresGaëtan Gilbert
2020-04-13test partial importGaëtan Gilbert
2020-04-13syntax for import filtersGaëtan Gilbert
2020-04-13correctly open objects for Names filtersGaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-13Add ExtRefMap/Set to globnamesGaëtan Gilbert
2020-04-13Add specific test for "useless" syndefGaëtan Gilbert
This happens in practice with the list syndef in List.v
2020-04-13dune states target: respect user's global verbosity settingGaëtan Gilbert
2020-04-13Merge PR #12087: Temporarily disable Windows job on Azure.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-13Temporarily disable Windows job on Azure.Théo Zimmermann
This job is currently broken because of Dune 2.5 not being available yet on the mingw-opam-repository. Before this, it was already red most of the time because of two issues: - Cygwin cannot be downloaded - "Error on dynamically loaded library: .\kernel/byterun\dllbyterun_stubs.dll: The specified module could not be found" bug." We don't know exactly when the latter appeared. It was missed because of the former. The goal is to reenable Windows testing based on standard opam with no cygwin. Hopefully, this is achievable in the next few weeks.
2020-04-13Merge PR #11539: [dune] [stdlib] Build the standard library natively with Dune.Théo Zimmermann
Reviewed-by: Zimmi48
2020-04-12[warnings] Be silent about the `set_tag` warning.Emilio Jesus Gallego Arias
This is a critical warning in terms of future compatibility but it makes no sense to be verbose about it every build.
2020-04-12[test-suite] Remove deprecated -I option of coqchk in MakefilePierre Roux
2020-04-11[dune] [doc] Remove the quick targets in favor of the shims.Emilio Jesus Gallego Arias
These targets are redundant with the shims. We also improve the documentation quite a bit.
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
This completes a pure Dune bootstrap of Coq. There is still the question if we should modify `coqdep` so it does output a dependency on `Init.Prelude.vo` in certain cases. TODO: We still double-add `theories` and `plugins` [in coqinit and in Dune], this should be easy to clean up. Setting `libs_init_load_path` does give a correct build indeed; however we still must call this for compatibility?
2020-04-11[ci] [build] Bump Dune to 2.5.0Emilio Jesus Gallego Arias
It is unfortunate that we cannot install coqide and Dune 2.5.0 in < 4.07.0
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10coqdoc: Report location of mismatched '[['Lysxia
2020-04-10[sideeff] Don't use polymorphic equality to check for empty side-effectsEmilio Jesus Gallego Arias
2020-04-10[proof] Introduce `prepare_proof` to improve normalization workflow.Emilio Jesus Gallego Arias
Old code was doing two passes on `initial_goals`; this produced some awkward situations code-wise. The `~unsafe_typ` parameter to `prepare` is needed to preserve the behavior introduced in bf0499bc507d5a39c3d5e3bf1f69191339270729 : > Do not normalize the type of a proof according to the final universes > when keep_body_ucst_separate is true, otherwise the type might not be > retypable in the initial context We need to investigate more, as of today we keep this behavior which seems to work.
2020-04-10Suppress the space after "#" when printing productionsJim Fehrle
to reflect lexer requirement for no space
2020-04-10Ignore subscripts in notation for matching cmds and tacsJim Fehrle
2020-04-10Fix prefix matchingJim Fehrle
2020-04-10Merge PR #12039: Do not erase native files in debug modePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-10Merge PR #11882: Adding a short form of Ltac2 Fresh.freshPierre-Marie Pédrot
Reviewed-by: MSoegtropIMC Reviewed-by: ppedrot Ack-by: tchajed
2020-04-10Merge PR #11756: [lib] Remove custom backtrace-destroying finalizersPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-10Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-cryptoGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-09Merge PR #12010: Remove dead code in Evarsolve alias algorithmHugo Herbelin
2020-04-09Code simplification in find_projectable_vars.Pierre-Marie Pédrot
We inline the "with_evars := false" case.
2020-04-09Remove a unused computation in alias code.Pierre-Marie Pédrot
The effects field of the UniqueProjection constructor was never accessed.
2020-04-09Inline an alias-computing function only used once.Pierre-Marie Pédrot
This makes some invariants explicit and is 1:1 equivalent.
2020-04-09Remove dead code in Evarsolve alias resolution.Pierre-Marie Pédrot
2020-04-09Merge PR #12046: [errors] Print backtrace of internal errors in printersPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-09Merge PR #11534: Support universe bindings and universe constraints in Let ↵Gaëtan Gilbert
definitions. Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:09:18 +0000