aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-03Remove a very specific low-level tactical from Refiner.Pierre-Marie Pédrot
It was only used at one point in the STM, and its localization was suprising to say the least. Furthermore it was relying on legacy code. Instead we hardcode it in the STM.
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
This function was used almost everywhere with the wrapper around.
2020-05-03Remove a critical call to V82.tactic in Clenvtac.Pierre-Marie Pédrot
Despite being marked as a breaking change by myself, it seems that the underlying condition had been solved in the meantime.
2020-05-02Merge PR #12172: Refactor first chapter: first step, the section on basics.Clément Pit-Claudel
Ack-by: JasonGross Ack-by: jfehrle
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-05-01Merge PR #12221: Replace QSeqEquiv by QCauchySeq, simplify proofs.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-01Preserve vernac chapter.Théo Zimmermann
2020-05-01Extract two new files out of Gallina chapter.Théo Zimmermann
2020-05-01Create section on writing libraries with only deprecated attributes.Théo Zimmermann
2020-05-01Extract deprecated attribute from Gallina chapter.Théo Zimmermann
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Remove lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Create basics out of sections from Gallina and Vernac chapters.Théo Zimmermann
2020-05-01Create section on basics with just flags, options and tables.Théo Zimmermann
2020-05-01Extract flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Create section on basics with just lexical conventions and attributes.Théo Zimmermann
2020-05-01Extract lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Merge PR #12217: Fix #12215: ci scripts naming inconsistenciesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-01Merge PR #12222: Less confusing configure message when lablgtk exists but ↵Emilio Jesus Gallego Arias
not lablgtksourceview Reviewed-by: ejgallego
2020-04-30Replace QSeqEquiv by QCauchySeq, simplify proofs.Vincent Semeria
Force Cauchy modulus equal to identity, make division transparent Fix test
2020-04-30Less confusing configure message when lablgtk exists but not lablgtksourceview.Hugo Herbelin
2020-04-30Merge PR #12213: [zify] add support for Nat.le, Nat.lt and Nat.eqVincent Laporte
Reviewed-by: vbgl
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2020-04-30Merge PR #12216: Remove outdated code and comments in Declare.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat. The required declarations are now added in ZifyInst.
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-30Remove outdated code and comments in Declare.Pierre-Marie Pédrot
Some comments referred to the old way of redeclaring constants at section closure. One of the comments was almost 20 years old...
2020-04-30Merge PR #12208: Reduce rational numbers in Cauchy real addition, to ↵Michael Soegtrop
accelerate it Reviewed-by: MSoegtropIMC
2020-04-29Merge PR #12209: Merge duplicates in .mailmapThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: rnrand
2020-04-29Merge duplicates in .mailmapJason Gross
I gave preference to the email address with the larger number of commits. To find duplicates, I used the script ```bash for i in $(git shortlog -nse | sed s'/^\s*[0-9]*\s*//g' | grep -o '^[^<]*' | sed s'/\s*$//g' | sed s'/ /,/g'); do if [ $(git shortlog -nse | sed s'/ /,/g' | grep -c "$i") -gt 1 ]; then git shortlog -nse | grep "$(echo "$i" | sed s'/,/ /g')"; fi; done ```
2020-04-29Reduce rational numbers in Cauchy real addition, to accelerate itVincent Semeria
2020-04-29Merge PR #11606: [tools] Add memory stats to tables by defaultEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-29Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor ↵Emilio Jesus Gallego Arias
in record tuples Reviewed-by: ejgallego
2020-04-29Merge PR #12198: CI: change ext-lib url, it is at coq-community nowEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-04-29Merge PR #12202: Centralize the call to `tclEFFECTS` in scheme declarationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-29Merge PR #12150: Support in-line glossary definitions and references with an ↵Clément Pit-Claudel
index Ack-by: Zimmi48
2020-04-29Merge PR #12158: [univ] API to demote global universesMatthieu Sozeau
Reviewed-by: mattam82
2020-04-29Merge PR #12195: [doc] [sphinx] Run in silent mode by defaultThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29Merge PR #12174: [ci] Add coq-tools to the CIThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29Support in-line glossary entries and referencesJim Fehrle
with an index
2020-04-29Merge PR #12203: [ci] [doc] misspelled script name create_overlays.shThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29[univ] API to demote global universesEnrico Tassi
2020-04-29correct script name create_overlays.shOlivier Laurent
2020-04-29Merge the call to tclEFFECTS into find_scheme.Pierre-Marie Pédrot
This encapsulates better the invariants of this function.
2020-04-29Remove dead user-facing code in scheme generation.Pierre-Marie Pédrot
It was trying to warn the user about missing schemes. Since find_scheme was generating those constants anyways, this was never reached.
2020-04-29CI: ext-lib is at coq-community nowAntonio Nikishaev
2020-04-28Merge PR #12193: Close files in fetch_delayedEmilio Jesus Gallego Arias
Ack-by: ejgallego Ack-by: ppedrot
2020-04-28[doc] [sphinx] Be silent when running latexmkEmilio Jesus Gallego Arias
This is actually supported by Sphinx directly.
2020-04-28[doc] [sphinx] Run in silent mode by defaultEmilio Jesus Gallego Arias
The convention in the dune build is to be silent except for warnings and errors, so they don't go unnoticed. We could have this controlled by a variable if needed (likely would require some support from Dune?) Solves part of #12194
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:26:48 +0000