aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-07-22Merge PR #10522: Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and ↵Maxime Dénès
Gappa) Reviewed-by: vbgl
2019-07-20Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg ↵Théo Zimmermann
files and insert it into .rst files Ack-by: Zimmi48 Ack-by: gares Ack-by: ppedrot
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
and inserting it into the .rst files
2019-07-19Merge PR #10521: Move unfold_side_flags CClosure -> Tacred internalsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-07-19Removed patches for Flocq, Interval and Gappa (merged upstream)Michael Soegtrop
2019-07-19Merge PR #10532: [doc] Fix typo in doc/sphinx/addendum/ring.rstthery
2019-07-18[doc] Fix typo in doc/sphinx/addendum/ring.rstWojciech Nawrocki
2019-07-17Merge PR #10518: [funind] Remove unneeded callback.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-07-17Fixed Windows patch for QuickchickMichael Soegtrop
2019-07-17Adjust VST patch to latest changes in VSTMichael Soegtrop
2019-07-17Make windows build fail immediately if plugin patches failMichael Soegtrop
2019-07-16Removed patch for Gappa tool (verified that changes in gappa master fixed ↵Michael Soegtrop
the windows crash)
2019-07-16Enable Coquelicot, Flocq, Interval and Gappa in extended/release Windows buildsMichael Soegtrop
2019-07-16Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)Michael Soegtrop
2019-07-16Move unfold_side_flags CClosure -> Tacred internalsGaëtan Gilbert
2019-07-16Merge PR #10520: Fix typosThéo Zimmermann
Reviewed-by: Zimmi48
2019-07-15TyposJim Fehrle
2019-07-15[funind] Remove unneeded callback.Emilio Jesus Gallego Arias
2019-07-15Merge PR #10517: Azure CI MacOS: build byte target firstEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-07-15Azure CI MacOS: build byte target firstGaëtan Gilbert
It looks like the recent spurious failures are because it somehow wants to build gramlib byte and opt at the same time and the old race condition causes the error. Having failed to debug the makefile, we work around by building byte first.
2019-07-15Merge PR #10512: Remove Stm.call_process_error_oncePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-07-14Merge PR #10496: [proof] Minor cleanup in proof.mlPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-07-11Merge PR #10424: Update doc for % escapes in Sphinx, improve error messagesClément Pit-Claudel
Reviewed-by: cpitclaudel
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-07-11Merge PR #10510: Fixed a few wrong reference and typosThéo Zimmermann
Reviewed-by: Zimmi48
2019-07-11Remove Stm.call_process_error_onceGaëtan Gilbert
This is the identity function since 07abf9818a6b47bb2c2bd0a8201da9743a0c10b6
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: ppedrot
2019-07-11Update doc/sphinx/proof-engine/ssreflect-proof-language.rstFlorent Hivert
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-07-11Merge PR #10439: Uniform handling of side-effects for opaque definitionsMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes
2019-07-10Fixed a few wrong reference and typosFlorent Hivert
2019-07-10Merge PR #10506: merge-pr.sh: filter reviews to remove the PR authorThéo Zimmermann
Reviewed-by: Zimmi48
2019-07-10Merge PR #10509: [CI/Azure/macOS] Attempt at pinning the homebrew-core ↵Emilio Jesus Gallego Arias
repository Reviewed-by: SkySkimmer Ack-by: ejgallego
2019-07-10[CI/Azure/macOS] Pin the homebrew-core repositoryVincent Laporte
This improves reproducibility of the CI environment. The chosen commit has GTK+3 at 2.24.9.
2019-07-10Merge PR #10446: [proof] Remove sign parameter to open_lemma.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-07-09merge-pr.sh: filter reviews to remove the PR authorGaëtan Gilbert
This removes spurious Ack-by lines
2019-07-09Merge PR #10471: [core] [api] Support OCaml 4.08Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2019-07-09[proof] Remove sign parameter to open_lemma.Emilio Jesus Gallego Arias
The current code does some "opacification" for `Let`s, however that's pretty fragile in general and not all codepaths do respect it. We need to decide what to do.
2019-07-09Merge PR #10453: [errors] Small cleanups and removal of dead code.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-07-09Merge PR #10067: Faster renaming of shadowed variables in evar instance ↵Hugo Herbelin
creation. Reviewed-by: herbelin
2019-07-08Adding a changelog.Pierre-Marie Pédrot
2019-07-08Similar purity invariants in the kernel.Pierre-Marie Pédrot
2019-07-08Further cleanup following the removal of pure opaque definitions.Pierre-Marie Pédrot
We can statically enforce that opaque definitions are always impure by means of typing, leading to quite a few simplifications.
2019-07-08Do not export side-effects of polymorphic definitions.Pierre-Marie Pédrot
This is the last call to the kernel that makes a difference between opaque definitions depending on their polymorphic status.
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
Not pretty, but it had to be done some day, as `Globnames` seems to be on the way out. I have taken the opportunity to reduce the number of `open` in the codebase. The qualified style would indeed allow us to use a bit nicer names `GlobRef.Inductive` instead of `IndRef`, etc... once we have the tooling to do large-scale refactoring that could be tried.
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
The changes are large due to `Pervasives` deprecation: - the `Pervasives` module has been deprecated in favor of `Stdlib`, we have opted for introducing a few wrapping functions in `Util` and just unqualified the rest of occurrences. We avoid the shims as in the previous attempt. - a bug regarding partial application have been fixed. - some formatting functions have been deprecated, but previous versions don't include a replacement, thus the warning has been disabled. We may want to clean up things a bit more, in particular w.r.t. modules once we can move to OCaml 4.07 as the minimum required version. Note that there is a clash between 4.08.0 modules `Option` and `Int` and Coq's ones. It is not clear if we should resolve that clash or not, see PR #10469 for more discussion. On the good side, OCaml 4.08.0 does provide a few interesting functionalities, including nice new warnings useful for devs.
2019-07-08Merge PR #10497: [lemmas] Move mutually recursive lemma analysis to its own ↵Gaëtan Gilbert
module. Reviewed-by: SkySkimmer
2019-07-08[errors] Small cleanups and removal of dead code.Emilio Jesus Gallego Arias
2019-07-08Merge PR #9686: [error] Remove special error printing pre-processingGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-07-08Merge PR #10466: [python] Remove use of generic python shebang, update CIGaëtan Gilbert
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2019-07-08Merge PR #10246: Investigations in the initialization of coq binaries and ↵Emilio Jesus Gallego Arias
command line (part 1) Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:08:58 +0000