aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-04Merge PR #12211: When TIMED=1, emit timing info for OCaml filesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-04Merge PR #12220: [dune] [doc] TweaksGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-04[dune] [doc] TweaksEmilio Jesus Gallego Arias
Close #12167
2020-05-03Merge PR #12231: Simplify division of Cauchy realsMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-05-03Merge PR #12238: [stdlib] [CPermutation] patch for #12031Hugo Herbelin
Reviewed-by: herbelin
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-03consistency with PermutationOlivier Laurent
2020-05-03Simplify division of Cauchy realsVincent Semeria
Improve comments
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-02Move tclWRAPFINALLY to profile_ltacJason Gross
As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef
2020-05-02Decrease LtacProf overhead when not profilingJason Gross
Note that this slightly changes the semantics of backtracking across `start ltac profiling`.
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
Fixes #12196
2020-05-02Add Proofview.tclWRAPFINALLYJason Gross
This new primitive (which could be implemented in terms of `tclCASE`, but which I believe encapsulates a useful unit of behavior) is needed for correctly implementing both `with_strategy` and for implementing multi-success support for the Ltac Profiler. The basic function of this tactical is to allow wrapping multi-success tactics with initialization and cleanup routines. For example, if `tac` is a multi-success tactic that writes its status to a log file, you might want to wrap `tac` in "first open the log file" and then after it runs "finally close the log file". (Unfortunately, the way the monad is set up doesn't allow passing data from the most recent run of the initializer to the tactic, which suggests that perhaps there's something a bit off about this abstraction. Perhaps we should set up a ref cell and that will hold the most recent return of the initializer and pass this ref cell to the wrapped tactic? But this can be done externally without needing to modify the current API. In any case, such data is not needed in the case of the Ltac Profiler, where the initializer is "update the current call stack and record the current start time" and the finalizer is "update the call stack and record the end time", and you want to have the start time be restarted when re-entering a tactic. Nor is it needed for `with_strategy` which needs to update the global conv_oracle so that it plays nicely with `abstract`.)
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-29When TIMED=1, emit timing info for OCaml filesJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:32:44 +0000