aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-28Merge PR #8826: [toplevel] Allow to specify default options.Pierre-Marie Pédrot
2018-11-27Added two proofs to the Lists library. The first, Forall_inv_tail, extends ↵llee454@gmail.com
Forall_inv to assert that a property that is true for every element of a list is true for every element in the tail of the list. The second, Exists_impl, parallels Forall_impl and proves that if there exists an element in a list that satisfies a given predicate, and the predicate implies another proposition, then there exists an element in the list that satisfies the implied proposition. Both of these proofs fill natural gaps within the List library.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-25 17:29:21 +0000