aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-28Merge PR #9089: Fix #9076 (warning appears when running test suite)Emilio Jesus Gallego Arias
2018-11-28[ltac] Remove aliases already present in the lower layers.Emilio Jesus Gallego Arias
We remove a few aliases present in the lower layers [`Genintern/Tactypes`] from `Tacexpr`. IMHO this enlarges the API for no good purpose, and difficults analysis.
2018-11-28[coq overlay] Adapt to coq/coq#8705Emilio Jesus Gallego Arias
Please apply when indicated.
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
This makes setting the option outside of the synchronized summary impossible.
2018-11-28[build] Test tests in Travis, use coqc for tests.Emilio Jesus Gallego Arias
`coqtop -batch` is an oxymoron, in prevision for upstream changes use `coqc`. We also call `make test` in Travis as to make CI more robust.
2018-11-27Merge PR #8854: Fix #8364: making univ algebraic when already equal to another.Matthieu Sozeau
2018-11-27Merge PR #9072: Clean stm flagsEnrico Tassi
2018-11-27[ci] [appveyor] Move Appveyor to OPAM 2.Emilio Jesus Gallego Arias
We update the Appveyor configuration so it uses OPAM 2.0, and thus it can install newer packages.
2018-11-27[lib] Remove leftover flag `print_mod_uid`Emilio Jesus Gallego Arias
The whole `native_name_from_filename` business seems quite strange tho.
2018-11-27[gramlib] Remove unused function `gram_reinit`.Emilio Jesus Gallego Arias
2018-11-27[pcoq] Remove a redundant `entry` type.Emilio Jesus Gallego Arias
This was done in a bit of redundant way when we removed the camlp4 compat layer; we fix this and make the type flow clearer.
2018-11-27[gramlib] Minor cleanups:Emilio Jesus Gallego Arias
- remove duplicate type definitions `gram_assoc`, `gram_position`, - make global `warning_verbose` variable into a parameter.
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a ↵Emilio Jesus Gallego Arias
write_function
2018-11-27Make `-async-proofs on` effective with `coqc`Maxime Dénès
Before this patch, it had no effect.
2018-11-27Remove -async-proofs-full flagMaxime Dénès
The semantics of this flag was not clear, it had several rather orthogonal effects. Also, it should probably have been another value of `-async-proofs-mode`, rather than a separate flag, as its combination with e.g. `-async-proofs-mode off` is unclear.
2018-11-27Merge PR #7033: Remove obsolete files from dev/docThéo Zimmermann
2018-11-27Fix #9076 (warning appears when running test suite)Maxime Dénès
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
When making a universe a variable we iterate through the universes we're equal to and if we find one we update the substitution accordingly. NB: The bug called make_flexible_variable on Top.15 and ~~~ {Top.15 Top.14} |= Top.11 < Top.6 Top.14 < Top.5 Top.11 = Top.15 ALGEBRAIC UNIVERSES:{Top.17 Top.16} UNDEFINED UNIVERSES:Top.17 := Top.14+1 Top.16 := Top.14+1 WEAK CONSTRAINTS: ~~~ so now we would add [Top.15 := Top.11].
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-27Merge PR #7696: Remove some univ_flexible_alg from casesPierre-Marie Pédrot
2018-11-27Merge PR #8255: Fast typing of application nodesMaxime Dénès
2018-11-27Merge PR #8986: Put -indices-matter in typing_flagsMaxime Dénès
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
This introduces the warning “not-a-class” in the “typeclasses” category.
2018-11-27Record.declare_class: remove unused “finite” parameterVincent Laporte
2018-11-27Merge PR #8686: [toplevel] Move compilation-related functions to their own ↵Pierre-Marie Pédrot
module.
2018-11-26Merge PR #9075: [ci] Set windows jobs to allow_failure: trueGaëtan Gilbert
2018-11-26Merge PR #9057: [nix-ci] Add a README in dev/ci/nixThéo Zimmermann
2018-11-26Merge PR #9063: [checker] Remove duplicated code from checker / clibPierre-Marie Pédrot
2018-11-26[dune] Minor tweak of dependencies.Emilio Jesus Gallego Arias
`clib` doesn't need `dynlink`, but `lib` does, similarly for `threads`, `num`... We align Dune and META deps.
2018-11-26[ci] Set windows jobs to allow_failure: trueEmilio Jesus Gallego Arias
Windows jobs have been polluting the CI for quite a few days, allow them to fail.
2018-11-26Merge PR #9074: Fix ocamldebug-coq for packed gramlibEmilio Jesus Gallego Arias
2018-11-26Fix ocamldebug-coq for packed gramlibGaëtan Gilbert
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-26[nix-ci] Add a README in dev/ci/nixVincent Laporte
2018-11-26[nix-ci] Use master version of UnicoqVincent Laporte
2018-11-26[ssreflect] Export more parsing witnesses.Emilio Jesus Gallego Arias
This is needed in order to serialize ssreflect programs properly, similar to #6795.
2018-11-25Merge PR #9036: Add bodies to sphinx objects.Clément Pit-Claudel
2018-11-25Merge pull request coq/ltac2#88 from wilcoxjay/tests-detect-coqbinPierre-Marie Pédrot
Autodetect COQBIN in tests/Makefile
2018-11-24tests/Makefile: support unset COQBIN, like top-level Makefile doesJames R. Wilcox
2018-11-24[toplevel] Allow to specify default options.Emilio Jesus Gallego Arias
In some cases, toplevel ML clients may want to modify the default set of flags that is passed to the main initalization routine. This is for example useful for `idetop` to suppress some undesired printing at startup. I would say that clients ought to have more control, but I do expect that PRs such as #8690 will help providing a better separation thus a mode orthogonal API.
2018-11-24[toplevel] Move compilation-related functions to their own module.Emilio Jesus Gallego Arias
We move compilation-specific functions to their own module. This helps isolating `.vo` compile-time functionality from interactive, toplevel-like processing. cc: #8683
2018-11-24[toplevel] Move command line path processing to CoqargsEmilio Jesus Gallego Arias
We move the processing of path-related arguments to `Coqargs`, and following experience from `SerAPI` we stored already-processed `coq_paths` in the `opts` record. This has proven to be very convenient as to avoid duplication of code in the presence of several clients of the `Coqargs` parsing functionality.
2018-11-24Merge PR #8996: Fix #8937: inductive conversion in coqchk subtypingHugo Herbelin
2018-11-24Merge PR #8950: [topfmt] Add phase attribute for toplevel printing.Hugo Herbelin
2018-11-24[checker] Remove duplicated from checker / clibEmilio Jesus Gallego Arias
Now that we link lib we can do this.
2018-11-24Merge pull request #18 from SkySkimmer/solve-remaining-evars-initial-argEmilio Jesús Gallego Arias
Adapt to coq/coq#8933 (Make initial evar map argument to check_evars_are_solved optional)
2018-11-24Merge PR #8929: Fix fixpoint related lifting in open recursors + related ↵Pierre-Marie Pédrot
cleanups
2018-11-24Merge PR #8933: Make initial evar map argument to check_evars_are_solved ↵Pierre-Marie Pédrot
optional.
2018-11-24Merge pull request coq/ltac2#87 from ppedrot/camlp5-safe-api-strikes-backPierre-Marie Pédrot
Fix w.r.t. coq/coq#9051.
2018-11-24Merge PR #9022: [ci] [doc] Split user/developer README, add info about ↵Théo Zimmermann
Nix/Docker CI
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-30 10:46:53 +0000