aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
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-10Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-cryptoGaëtan Gilbert
Reviewed-by: SkySkimmer
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.
2020-04-06Merge PR #12006: [coq_makefile] remove .lia.cache and .nia.cache by make ↵Enrico Tassi
cleanall Reviewed-by: gares
2020-04-06Clean and fix definitions of options.Théo Zimmermann
- Provide new helper functions in `Goptions` on the model of `declare_bool_option_and_ref`; - Use these helper functions in many parts of the code base (encapsulates the corresponding references); - Move almost all options from `declare_string_option` to `declare_stringopt_option` (only "Warnings" continue to use the former). This means that these options now support `Unset` to get back to the default setting. Note that there is a naming misalignment since `declare_int_option` is similar to `declare_stringopt_option` and supports `Unset`. When "Warning" is eventually migrated to support `Unset` as well, we can remove `declare_string_option` and rename `declare_stringopt_option` to `declare_string_option`. - For some vernac options and flags that have an equivalent command-line option or flag, implement it like the standard `-set` and `-unset`.
2020-04-06Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_stateMatthieu Sozeau
Reviewed-by: SkySkimmer Reviewed-by: mattam82
2020-04-05Merge PR #12025: Fixes #11194 (Canonical/Coercion not located for coqdoc)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-05Fixes #11194 (Canonical/Coercion not located for coqdoc).Hugo Herbelin
The location was missing in the parser.
2020-04-03Avoiding using a fixed introduction name in Ltac code of stdlib.Hugo Herbelin
2020-04-03Adding change log.Hugo Herbelin
2020-04-03Adding fresh-in-context: a short form of Ltac2 Fresh.fresh.Hugo Herbelin
2020-04-03Fix the test for bug #4544.Pierre-Marie Pédrot
It seems that this PR is making the rewrite much, much faster.
2020-04-03Be cleverer and do not hopelessly rezip a term when not needed.Pierre-Marie Pédrot
A quick analysis showed that most of the calls to whd do not lead to a term which further triggers reduction, so there is no point in refolding a potentiall huge term for no reason.
2020-04-03Use the kernel machine in whd_betaiota_deltazeta_for_iota_state.Pierre-Marie Pédrot
There is no point in using the exaggerately inefficient Reductionops machine. We need to be call-by-name to preserve the shape of the reduced terms, as call-by-need would introduce sharing and thus at-distance effects in term refolding. Yet, the Reductionops machine is worse than that, since it performs substitutions eagerly, leading to a catastrophical performance profile. Instead, we use the kernel reduction in by-name mode to replace the Reductionops machine in whd_betaiota_deltazeta_for_iota_state with all flags on. Since the kernel is using explicit substitutions, this is algorithmically more efficient. Apart from minor differences, this should produce the same normal form. As showed by the benchmarks, this is a critical change for the odd-order proofs. Ideally, we should use delayed substitutions in the Reductionops machine as well for great profit, but due to code entanglement this is a much less self-contained change.
2020-04-03Merge PR #12007: Fix CoRN & Flocq CI scripts.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-03Fix Flocq CI script.Théo Zimmermann
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
2020-04-03Merge PR #11664: Encoding string list as a string with application to the ↵Emilio Jesus Gallego Arias
parsing of coqtop arguments in coqide Reviewed-by: ejgallego
2020-04-03Merge PR #11895: Remove Chapter command.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-03Merge PR #11914: Start the split of the Gallina Extensions chapter.Clément Pit-Claudel
Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:32:22 +0000