aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2020-04-09Merge PR #11534: Support universe bindings and universe constraints in Let ↵Gaëtan Gilbert
definitions. Reviewed-by: SkySkimmer
2020-04-09Merge PR #12056: [pre-commit] Check ocamlformat version and silence ocamlformat.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-04-09Merge PR #12050: Fix a typo in CoqMakefile.inPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-09[pre-commit] Check ocamlformat version and silence ocamlformat.Théo Zimmermann
Cf. #12049.
2020-04-08Merge PR #12044: proposed fix for the issue #12015 (String_as_OT)Jason Gross
Reviewed-by: JasonGross
2020-04-08[ci] [fiat-crypto] [flambda] Don't use flambda for fiat-cryptoEmilio Jesus Gallego Arias
As of today flambda is pretty stack-hungry for some developments, in particular it doesn't work [`StackOverflow` in fiat-crypto extracted code even with large stacks. We are thus forced to revert fiat-crypto's compilation to the regular OCaml compiler. This is OCaml bug https://github.com/ocaml/ocaml/issues/7842
2020-04-08Merge PR #11909: Make the level of ≡ in Int63 consistent with =Hugo Herbelin
Reviewed-by: anton-trunov
2020-04-08Fix a typo in CoqMakefile.inJason Gross
2020-04-08[errors] Print backtrace of internal errors in printersEmilio Jesus Gallego Arias
This is useful as witnessed by #11829 , as some errors printers do still fail, so it costs little to have both backtraces.
2020-04-08Merge PR #12005: Remove deprecated coqtop optionsEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: ejgallego
2020-04-07Merge PR #11997: Clean and fix definitions of options.Emilio Jesus Gallego Arias
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: gares Ack-by: jfehrle
2020-04-07Integrated changes proposed by @JasonGrossilya
2020-04-07proposed fix for the issue #12015 (String_as_OT)ilya
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants.
2020-04-07Merge PR #12042: Fix documentation of Print Libraries following #10476.Clément Pit-Claudel
2020-04-07Fix documentation of Print Libraries following #10476.Théo Zimmermann
2020-04-07Do not erase native files in debug modeMaxime Dénès
Being able to inspect the generated OCaml code is a useful debug tool. It seems this was disabled by mistake in #11081.