aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-05-23Merge PR #10217: Less undefined tokensClément Pit-Claudel
Ack-by: JasonGross Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2019-05-23Merge PR #10227: Update `Bind Scope` documentation to reflect dynamic ↵Théo Zimmermann
binding semantics. Ack-by: Zimmi48
2019-05-23Suggestions from review.Théo Zimmermann
Co-authored-by: Jason Gross <jgross@mit.edu>
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ↵Maxime Dénès
vernac Reviewed-by: maximedenes
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-05-23Update doc/sphinx/user-extensions/syntax-extensions.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-05-23More misc refman fixes, less undefined tokens.Théo Zimmermann
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
2019-05-23Update `Bind Scope` documentation to reflect ↵Maxime Dénès
3d09e39dd423d81c6af3e991d5b282ea8608646b The commit mentioned above changed the semantics of `Bind Scope` to a dynamic binding behavior. It forgot to update the documentation. Fixes #10064
2019-05-23Merge PR #10221: Fixing typos - Part 2 (reopening of #10218)Théo Zimmermann
2019-05-23Merge PR #10192: More miscellaneous refman fixes (reopened version of #10187)Théo Zimmermann
Ack-by: Zimmi48
2019-05-23Merge PR #10214: Better dune ocamldebug integrationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: vbgl
2019-05-23Merge PR #8768: [stm] Add hooks for document actions.Enrico Tassi
Reviewed-by: gares
2019-05-23Fixing typos - Part 2JPR
2019-05-22Fix ambiguous comment problemTalia Ringer
2019-05-22unified style for new hooks and old hooksTalia Ringer
2019-05-22Merge PR #10173: Fail: don't catch critical errorsEmilio Jesus Gallego Arias
2019-05-22Merge remote-tracking branch 'origin/master' into stm+doc_hookTalia Ringer
2019-05-22Better dune ocamldebug integrationGaëtan Gilbert
- use coqc instead of coqtop (since -compile doesn't work anymore this is better) - pass through extra arguments to dune-dbg - auto detect the need to pass -emacs to ocamldebug - instructions for emacs users The dune-dbg dependencies are still broken ;_;
2019-05-22[refman] Add more missing @ signsClément Pit-Claudel
2019-05-22[refman] Misc fixes (mostly missing '@' signs)Clément Pit-Claudel
Co-Authored-By: @Zimmi48
2019-05-22[refman] Give explicit names to the various 'Arguments' commandsClément Pit-Claudel
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based ↵Hugo Herbelin
generalization + cleanups Reviewed-by: herbelin
2019-05-22Merge PR #10211: Use grep in changelog test instead of adhoc readsThéo Zimmermann
Reviewed-by: Zimmi48
2019-05-22Merge PR #10203: Fixing typos - Part 1Théo Zimmermann
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: gares Reviewed-by: jfehrle Reviewed-by: vbgl
2019-05-22Merge PR #10178: Improve doc for generalizing bindersThéo Zimmermann
Reviewed-by: Zimmi48
2019-05-22Use grep in changelog test instead of adhoc readsGaëtan Gilbert
2019-05-22Improve doc for generalizing bindersGaëtan Gilbert
2019-05-22Merge PR #10207: Partly revert micromega parsing using typeclasses.Vincent Laporte
Reviewed-by: vbgl
2019-05-22Merge PR #9980: [ci] Set artifact expire date for all jobs.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
Typeclasses resolution is not used anymore for lia. Typeclasses resolution is still used by lra but only to access a database of declared constants.
2019-05-22Update build-system.txtFourchaux
2019-05-21Fixing typos - Part 1JPR
2019-05-21[ci] Set artifact expire date for all jobs.Emilio Jesus Gallego Arias
Closes #8735 .
2019-05-21[loadpath] Factor in common logic for vio/vo file selection.Emilio Jesus Gallego Arias
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged.
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
We consolidate loadpath handling as a single `Loadpath` module from parts in `Library` and `Mltop`, placing it at the `vernac` level [as `Mltop`] This idea was first suggested in https://github.com/coq/coq/pull/9808 , and indeed it makes sense as library resolution tends to be business of the upper layers: IDE / build tools. Logic could be pushed upwards, but this is good enough for now. This consolidation has enabled some good and long overdue refactorings, and the module should become self-contained enough as to allow the resolution logic to be shared with `coqdep` in the future. The `Mltop` module only cares now about ML-level modules, and should go away once we rewrite the loader using `findlib` to solve https://github.com/coq/coq/issues/7698 .
2019-05-21Merge PR #10188: Remove definition-not-visible warningEmilio Jesus Gallego Arias
Reviewed-by: gares
2019-05-21Merge PR #10160: Miscellaneous fixes related to the command lineVincent Laporte
Ack-by: gares Ack-by: herbelin Reviewed-by: vbgl
2019-05-21Overlay for definition-not-visible overhaulGaëtan Gilbert
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
This lets us avoid passing ~ontop to do_definition and co, and after #10050 to even more functions.
2019-05-21Overlay for removing Instance: !type syntaxGaëtan Gilbert
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
It's used a few times in the stdlib (a couple of which need no other change when removing the !) and not at all throughout our CI. Considering that I think it's fair enough to remove it.
2019-05-21Merge PR #10042: [Classes] Use prepare_parameter from DeclareDef.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-21Merge PR #10174: Further cleanup of the side-effect machineryGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: maximedenes
2019-05-21Merge PR #10144: Fix #9919: conversion functions are non-linearHugo Herbelin
Ack-by: herbelin Reviewed-by: maximedenes Ack-by: ppedrot
2019-05-20[Classes] Use prepare_parameter from DeclareDef.Emilio Jesus Gallego Arias
This code was originally part of #8811, authored by Gaëtan Gilbert. It seems we are not very consistent on what we do when we use `ParameterEntry`, specially w.r.t. universes but as code cleanup progresses we will have a better view. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2019-05-20Do not perform the section variable check on global recipes.Pierre-Marie Pédrot
By construction, we know that Cooking is returning the right set of used variables. This set has been checked already once at the time when the definition was performed inside the section.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 21:18:06 +0000