| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-04-12 | Fixing 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 Makefile | Pierre 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.0 | Emilio 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-11 | Merge PR #11961: Convert vernac commands chapter to prodn, update syntax | Théo Zimmermann | |
| Ack-by: Zimmi48 Ack-by: cpitclaudel | |||
| 2020-04-11 | add properties of operations on vectors | Olivier Laurent | |
| 2020-04-11 | Fix #7812 | Attila Gáspár | |
| 2020-04-11 | If 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-11 | If 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-11 | Renaming confusingly-named insert_coercion into insert_entry_coercion. | Hugo Herbelin | |
| This is to avoid confusion with typing coercions. No change of semantics. | |||
| 2020-04-10 | Convert vernac commands chapter to prodn, update syntax | Jim Fehrle | |
| 2020-04-10 | coqdoc: Report location of mismatched '[[' | Lysxia | |
| 2020-04-10 | [sideeff] Don't use polymorphic equality to check for empty side-effects | Emilio 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-10 | Suppress the space after "#" when printing productions | Jim Fehrle | |
| to reflect lexer requirement for no space | |||
| 2020-04-10 | Ignore subscripts in notation for matching cmds and tacs | Jim Fehrle | |
| 2020-04-10 | Fix prefix matching | Jim Fehrle | |
| 2020-04-10 | Merge PR #12039: Do not erase native files in debug mode | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-04-10 | Merge PR #11882: Adding a short form of Ltac2 Fresh.fresh | Pierre-Marie Pédrot | |
| Reviewed-by: MSoegtropIMC Reviewed-by: ppedrot Ack-by: tchajed | |||
| 2020-04-10 | Merge PR #11756: [lib] Remove custom backtrace-destroying finalizers | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-04-10 | Change log for #12068 (Coqide segfault tentative fix). | Hugo Herbelin | |
| 2020-04-10 | Coqide 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-10 | Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-crypto | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2020-04-10 | [obligations] Deprecated flag cleanup | Emilio 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-09 | Merge PR #12010: Remove dead code in Evarsolve alias algorithm | Hugo Herbelin | |
| 2020-04-09 | Code simplification in find_projectable_vars. | Pierre-Marie Pédrot | |
| We inline the "with_evars := false" case. | |||
| 2020-04-09 | Remove a unused computation in alias code. | Pierre-Marie Pédrot | |
| The effects field of the UniqueProjection constructor was never accessed. | |||
| 2020-04-09 | Inline an alias-computing function only used once. | Pierre-Marie Pédrot | |
| This makes some invariants explicit and is 1:1 equivalent. | |||
| 2020-04-09 | Remove dead code in Evarsolve alias resolution. | Pierre-Marie Pédrot | |
| 2020-04-09 | Merge PR #12046: [errors] Print backtrace of internal errors in printers | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-04-09 | Merge PR #11534: Support universe bindings and universe constraints in Let ↵ | Gaëtan Gilbert | |
| definitions. Reviewed-by: SkySkimmer | |||
| 2020-04-09 | Merge PR #12056: [pre-commit] Check ocamlformat version and silence ocamlformat. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2020-04-09 | Merge PR #12050: Fix a typo in CoqMakefile.in | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2020-04-09 | [pre-commit] Check ocamlformat version and silence ocamlformat. | Théo Zimmermann | |
| Cf. #12049. | |||
| 2020-04-08 | Merge 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-crypto | Emilio 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-08 | Merge PR #11909: Make the level of ≡ in Int63 consistent with = | Hugo Herbelin | |
| Reviewed-by: anton-trunov | |||
| 2020-04-08 | Fix a typo in CoqMakefile.in | Jason Gross | |
| 2020-04-08 | [errors] Print backtrace of internal errors in printers | Emilio 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-08 | Merge PR #12005: Remove deprecated coqtop options | Emilio Jesus Gallego Arias | |
| Ack-by: SkySkimmer Ack-by: ejgallego | |||
| 2020-04-07 | Merge 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-07 | Integrated changes proposed by @JasonGross | ilya | |
| 2020-04-07 | proposed fix for the issue #12015 (String_as_OT) | ilya | |
| 2020-04-07 | Support 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-07 | Merge PR #12042: Fix documentation of Print Libraries following #10476. | Clément Pit-Claudel | |
| 2020-04-07 | Fix documentation of Print Libraries following #10476. | Théo Zimmermann | |
| 2020-04-07 | Do not erase native files in debug mode | Maxime 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. | |||
