aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2018-11-28Merge PR #8826: [toplevel] Allow to specify default options.Pierre-Marie Pédrot
2018-11-27Added two proofs to the Lists library. The first, Forall_inv_tail, extends Fo...llee454@gmail.com
2018-11-28Merge PR #9089: Fix #9076 (warning appears when running test suite)Emilio Jesus Gallego Arias
2018-11-28[ltac] Remove aliases already present in the lower layers.Emilio Jesus Gallego Arias
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-27Merge PR #8854: Fix #8364: making univ algebraic when already equal to another.Matthieu Sozeau
2018-11-27Merge PR #9072: Clean stm flagsEnrico Tassi
2018-11-27[ci] [appveyor] Move Appveyor to OPAM 2.Emilio Jesus Gallego Arias
2018-11-27[lib] Remove leftover flag `print_mod_uid`Emilio Jesus Gallego Arias