aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-12-04Merge PR #8187: Notation printing based on scopes (take 2, including bug fixes)Emilio Jesus Gallego Arias
2018-12-04Remove leftover code that used to handle ml4 files.Pierre-Marie Pédrot
2018-12-04Merge PR #9053: Document code owner team creation.Maxime Dénès
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
2018-12-04Notation.ml: Moving code about binding scopes to coercion classes earlier.Hugo Herbelin
2018-12-04Fixing missing newline in display of Locate for notations.Hugo Herbelin
2018-12-04Printing priority to most recent notation in case of non-open scopes with delim.Hugo Herbelin
2018-12-04Documentation of the rules for printing notations depending on scopes.Hugo Herbelin
2018-12-04Using scope for printing: more tests.Hugo Herbelin
2018-12-04Fixing #8551 (missing delimiters when notation exists both lonely and in scope).Hugo Herbelin
2018-12-04Addressing issues with PR#873: performance and use of abbreviation for printing.Hugo Herbelin
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
2018-12-04Pre-isolating a notation test to avoid interferences.Hugo Herbelin
2018-12-03Merge PR #9121: Closes #9118: single backticks are made equivalent to double ...Clément Pit-Claudel
2018-12-03[sphinx] Same rendering for :n:`@token` and :token:`token`.Théo Zimmermann
2018-12-03A few fixes of unexisting tokens.Théo Zimmermann
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try t...Théo Zimmermann
2018-12-03Merge PR #9119: [gitlab-ci] Increase git depth.Gaëtan Gilbert
2018-12-03Merge PR #9112: [release doc] vX.X branches are now automatically protected.Maxime Dénès
2018-11-30[vernac] [hooks] Refactor towards optional hooks.Emilio Jesus Gallego Arias
2018-11-30[gramlib] Remove `Ploc.t` in favor of `Loc.t`Emilio Jesus Gallego Arias
2018-11-30Merge PR #9068: [dune] Minor tweak of dependencies.Théo Zimmermann
2018-11-30[gitlab-ci] Increase git depth.Théo Zimmermann
2018-11-30Merge PR #8807: Added two proofs to the Lists library: Forall_inv_tail and Ex...Pierre-Marie Pédrot
2018-11-30Merge PR #9105: Add indexes for coercion / substructure symbol :>.Clément Pit-Claudel
2018-11-30Merge PR #9109: Fix numeral notations doc by indentingThéo Zimmermann
2018-11-30Merge PR #9102: [ltac] Remove aliases already present in the lower layers.Pierre-Marie Pédrot
2018-11-30Merge PR #9064: [gramlib] Minor cleanups:Pierre-Marie Pédrot
2018-11-30Merge PR #9104: coqide: Remove unused win32_kill C functionPierre-Marie Pédrot
2018-11-30Add indexes for coercion / substructure symbol :>.Théo Zimmermann
2018-11-29[release doc] vX.X branches are now automatically protected.Théo Zimmermann
2018-11-29Merge PR #9054: [ci] [appveyor] Move Appveyor to OPAM 2.Maxime Dénès
2018-11-28Fix numeral notations doc by indentingJason Gross
2018-11-28Merge PR #9070: [ssreflect] Export more parsing witnesses.Enrico Tassi
2018-11-28Add a couple more printing tests for byte/asciiJason Gross
2018-11-28Byte.v: use right-associative tuples in bitsJason Gross
2018-11-28Fix string notation docJason Gross
2018-11-28Proofs to ensure that conversions round-tripJason Gross
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-11-28Add extraction directives for nicer extraction of bytesJason Gross
2018-11-28Speed up ByteJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-28Merge PR #9041: [Windows CI] Do not build any addon if WINDOWS is not enabled...Michael Soegtrop
2018-11-28Merge PR #7153: Make OrderedTypeFullFacts a module functorGaëtan Gilbert
2018-11-28Remove Windows from allow_failure now that addons are not tested on PRs.Théo Zimmermann
2018-11-28[Windows CI] Do not build any addon if WINDOWS is not enabled_all_addons.Théo Zimmermann
2018-11-28coqide: Remove unused win32_kill C functionGaëtan Gilbert
2018-11-28Merge PR #9094: [lib] Remove leftover flag `print_mod_uid`Maxime Dénès
2018-11-28Merge PR #8727: [options] New helper for creation of boolean options plus ref...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 20:00:50 +0000