aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-15Making type interning_data abstract in constrintern.ml.Hugo Herbelin
2020-04-15Small convenient code factorization in constrintern.ml.Hugo Herbelin
No change of semantics.
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-13Remove documentation for Hide menu in CoqIDE (was removed in 8.5).Théo Zimmermann
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
2020-04-13Simplifying the declaration of constants bound to primitive projections.Hugo Herbelin
We factorize code from declareInd.ml and inductiveops.ml which was already existing in record.ml. We keep expansion of local definitions in the type of fields of primitive records while these are not expanded in the non-primitive case. This is to be consistent with what Indtypes.compute_projections is doing. See discussion at #11135. We keep the unused code from inductiveops.ml for possible future use though. Include improvements contributed by Gaëtan Gilbert.
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-12Tweak grammar to make doc_grammar happyJim Fehrle
2020-04-12CoqIDE completion: Relying on INSERT mark of the buffer.Hugo Herbelin
The iterator of the completion context does not seem trustable.
2020-04-12Exporting BEST as OPT for the tests using coq_makefile-generated Makefile.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 23:02:26 +0000