aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-01Changing fixpoint message "decreasing" -> "guarded".Hugo Herbelin
This is to be compatible with the possibility of having non truly recursive fixpoints.
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
There was also a non truly recursive in the doc.
2020-05-01Warn when a (co)fixpoint is not truly recursive.Hugo Herbelin
2020-05-01Slight modification of the partial-order algorithm so that it does notHugo Herbelin
remove itself in the set of elements bigger than it if it is indeed the case. This does not impact the warning issued when the recursivity is not mutual but this produces a result consistent with the unary case when the order is reflexive (i.e. results of the form (x,Inr[x,y]) happens also in the mutual case to indicate a cycle x<=y<=x while before we had results of the form (x,Inr[x]) only in the unary case). I.e.: Before: (x,[y]),(y,[x]) -> (x,Inr[]),(y,Inl x) (x,[x]) -> (x,Inr[x]) Now: (x,[y]),(y,[x]) -> (x,Inr[x]),(y,Inl x) (x,[x]) -> (x,Inr[x])
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-05-01do not re-export ListNotations from Program: vst overlayAntonio Nikishaev
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-30Move availability_of_prim_tokenPierre Roux
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-30Symmetry in conclusions of List.map_eq_*Olivier Laurent
allow simplified iterated applications
2020-04-30Merge PR #12208: Reduce rational numbers in Cauchy real addition, to ↵Michael Soegtrop
accelerate it Reviewed-by: MSoegtropIMC
2020-04-30do not re-export ListNotations from Program: fix testsuiteAntonio Nikishaev
2020-04-30do not re-export ListNotations from Program: changelogAntonio Nikishaev
2020-04-30do not re-export ListNotations from Program: overlaysAntonio Nikishaev
2020-04-30do not re-export ListNotations from ProgramAntonio Nikishaev
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 05:46:47 +0000