aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-04-12Fixing export of CAML_LD_LIBRARY_PATH from config/Makefile to Makefile.common.Hugo Herbelin
There were single quotes which were not interpreted in "PATH" syntax.
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-11[gitlab-ci] Only run Windows jobs when ONLY_WINDOWS variable is true.Théo Zimmermann
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-11add properties of operations on vectorsOlivier Laurent
2020-04-11Fix #7812Attila Gáspár
2020-04-11If a custom entry has global, a bound variable is valid in this entry.Hugo Herbelin
This is due to "global" being a syntactic notation, thus including ident. Parsing was automatically supporting this. This commit adds support for printing.
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ↵Hugo Herbelin
entry. Parsing was automatically supporting this. This commit adds support for printing. Note: It would be more delicate to recognize that some given entry support applicative nodes hence abbreviations with arguments.
2020-04-11Renaming confusingly-named insert_coercion into insert_entry_coercion.Hugo Herbelin
This is to avoid confusion with typing coercions. No change of semantics.
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-10Change log for #12068 (Coqide segfault tentative fix).Hugo Herbelin
2020-04-10Coqide completion: Avoiding using an iterator in an apparently sensitive code.Hugo Herbelin
Let's see if it fixes #11943. See there for explanations about the related segfault.
2020-04-10Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-cryptoGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
We deprecate `Hide Obligations` and remove `Shrink Obligations` [deprecated since 8.7]
2020-04-10[ocamlformat] Enable for funind.Emilio Jesus Gallego Arias
As part of the proof refactoring work I am doing some modifications to `funind` and indentation of that code is driving me a bit crazy; I'd much prefer to delegate it to an automatic tool.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 01:31:09 +0000