aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-07-23[funind] Remove single-shot type alias.Emilio Jesus Gallego Arias
Pointed out by Gaëtan Gilbert.
2019-07-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
We continue over the previous commit and remove redundant `structured_fixpoint_expr` record in favor of the one used in the AST. This removes some term-shuffling, tho we still have discrepancies related to adjustments on the recursive annotation.
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
We turn the tuples used for (co)-fixpoints into records, cleaning up their users. More cleanup is be possible, in particular a few functions can now shared among co and fixpoints, also `structured_fixpoint_expr` could like be folded into the new record. Feedback on the naming of the records fields is welcome. This is a step towards cleaning up code in `funind`, as it is the main consumer of this data structure, as it does quite a bit of fixpoint manipulation. cc: #6019
2019-07-23Merge PR #10541: Dune: fix build_all_stdlib ruleEmilio Jesus Gallego Arias
Ack-by: ejgallego
2019-07-22Merge PR #10447: Refactor and expand contributing guide.Maxime Dénès
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: jfehrle
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: mattam82
2019-07-22Merge PR #10462: [Pretyping] Do not restrict a solved evarEnrico Tassi
Reviewed-by: gares
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-22[Pretyping] Do not use the stale evarmap (in thin_evars)Vincent Laporte
Fixes #10300 and #10285.
2019-07-21Dune: do not use with-outputs-to for shimsGaëtan Gilbert
We only want stdout, so if there's something in stderr it will both make a wrong output and make it harder to debug.
2019-07-21Dune: fix build_all_stdlib ruleGaëtan Gilbert
The issue could be reproduced by doing "dune build test-suite/misc/universes/all_stdlib.v" (from a clean build) which would error 127 with no message. - only redirect stdout so that in the future we will see error messages - put the script as a dependency (I guess it sometime succeeded when copying the deps for the test suite happened before running it)
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-18Adding overlays.Pierre-Marie Pédrot
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-18Polymorphism attribute on section sets the option locally.Pierre-Marie Pédrot
This is deemed to be more natural as most of the uses will follow this structure.
2019-07-18Remove dead code in Lib.Pierre-Marie Pédrot
The polymorphic flag is now carried by the section rather than individual variables, no need to pass it along.
2019-07-18Attach the universe polymorphic status to sections.Pierre-Marie Pédrot
The previous implementation allowed to dynamically decide whether a section would be monomorphic or polymorphic at the first definition of a variable or a constraint. Instead of relying on this delayed decision, we set the universe polymorphic property directly at the time of the section definition.
2019-07-18Use a dedicated data structure for section representation in Lib.Pierre-Marie Pédrot
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-11Refactor the part about contributing to the stdlib.Théo Zimmermann
- Remove reference to the age of the stdlib - Remove reference to stdlib2 until it accepts contributions - Merge two paragraphs together - Minor wording improvements
2019-07-11More positive wording of the foreword to the contributing guide.Théo Zimmermann
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2019-07-11Improve contributing guide further following reviewers' comments.Théo Zimmermann
Thanks to the reviewers: Jim Fehrle, Emilio Gallego, Gaëtan Gilbert, Enrico Tassi.
2019-07-11Refactor and expand contributing guide.Théo Zimmermann
This is almost a full rewrite of the contributing guide. The goal was to have a more structured, and more exhaustive guide, where all our processes are documented, and from which all the useful documentation is linked to. The document lists contribution types in the order in which it is most natural to go through them: from contributions to the ecosystem, to issues, to code contributions, to taking part in the maintenance. However, it seemed important to not neglect this last part if we want to ease the onboarding of new maintainers (and not just of occasional contributors). A table of content makes it easy to go through the document (which is too long to be read from begin to end). The guide documents our processes in the way they are today, without changing anything, but this should be a good basis to make them evolve in the future. Insufficiently documented tools and processes are mentioned as such.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:37:11 +0000