aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
Reviewed-by: SkySkimmer Ack-by: herbelin Reviewed-by: ppedrot
2020-04-16Merge PR #12069: [gitlab-ci] Only run Windows jobs when ONLY_WINDOWS ↵Gaëtan Gilbert
variable is true. Reviewed-by: gares
2020-04-16Merge PR #11982: Fix #11854 error message on unsolved evars in Instance.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-16Merge PR #12101: Add needed commas in messageGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-16Merge PR #11999: [proof] Merge `Proof_global` into `Declare`Gaëtan Gilbert
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-04-15Add needed commas in messageJim Fehrle
2020-04-15[tmp] Compat API for CIEmilio Jesus Gallego Arias
Rewriter needs a bit of work as it calls a removed function, but no big deal.
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
This still needs API cleanup but we defer it to the moment we are ready to make the internals private.
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
This makes the API more orthogonal and allows better structure in future code.
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
If we remove all the legacy proof engine stuff, that would remove the need for the view on proof almost entirely.
2020-04-15[proofs] Move pfedit to `proofs`Emilio Jesus Gallego Arias
It seems to belong there, not in `tactics`
2020-04-15[declare] [abstract] Do evars check in declare_abstractEmilio Jesus Gallego Arias
This makes sense as it is mandatory for the client.
2020-04-15[declare] Mark APIs as scheduled for removal; remove a couple.Emilio Jesus Gallego Arias
We mark all the stuff scheduled to disappear in `Declare`, and remove a couple of non-needed APIs.
2020-04-15[dev] [doc] Changes.Emilio Jesus Gallego Arias
2020-04-15[proof] [abstract] Move internal declaration code to `Declare`Emilio Jesus Gallego Arias
As we are aiming to forbid low-level manipulation of proofs outside `Declare`, we move the code from `Abstract` to `Declare`. We remove `build_constant_by_tactic` from the public API.
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
We place creation and saving of interactive proofs in the same module; this will allow to make `proof_entry` private, improving invariants and control over clients, and to reduce the API [for example next commit will move abstract declaration into this module, removing the exported ad-hoc `build_constant_by_tactic`] Next step will be to unify all the common code in the interactive / non-interactive case; but we need to tweak the handling of obligations first.
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
This actually gets `Pfedit` out of the dependency picture [can be almost merged with `Proof` now, as it is what it manipulates] and would allow to reduce the exported low-level API from `Proof_global`, as `map_fold_proof` is not used anymore.
2020-04-15Ignore -native-compiler option when disabledPierre Roux
2020-04-15Merge PR #11776: [ocamlformat] Enable for funind.Pierre Courtieu
Reviewed-by: Matafou Ack-by: Zimmi48 Ack-by: maximedenes
2020-04-14Merge PR #11957: [stdlib] update sigma-type notationsHugo Herbelin
Reviewed-by: JasonGross Ack-by: herbelin
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-13Fix #11854 error message on unsolved evars in Instance.Gaëtan Gilbert
2020-04-13Fix #11783 Require in SectionGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:57:01 +0000