aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-12-05Merge PR #8911: Document undocumented flags and optionsThéo Zimmermann
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
Also remove a few undocumented settings
2018-12-04Remove undocumented "Proof using Clear Unused" flagJim Fehrle
2018-12-04Merge PR #9134: CI: track dev branch of coq-simple-ioEmilio Jesus Gallego Arias
2018-12-04CI: track dev branch of coq-simple-ioYishuai Li
2018-12-04Merge PR #9127: Remove leftover code that used to handle ml4 files.Emilio Jesus Gallego Arias
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
Namely, it does not explicitly open a scope, but we remember that we don't need the %type delimiter when in type position.
2018-12-04Notation.ml: Moving code about binding scopes to coercion classes earlier.Hugo Herbelin
We shall need it for changing the semantics of type_scope.
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
This modifies the strategy in previous commits so that priorities are as before in case of non-open scopes with delimiters. Additionally, we document the rare situation of overlapping applicative notations (maybe this is too rare and ad hoc to be worth being documented though).
2018-12-04Documentation of the rules for printing notations depending on scopes.Hugo Herbelin
Mostly courtesy of Jason Gross.
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
We do a couple of changes: - Splitting notation keys into more categories to make table smaller. This should (a priori) make printing faster (see #6416). - Abbreviations are treated for printing like single notations: they are pushed to the scope stack, so that in a situation such as Open Scope foo_scope. Notation foo := term. Open Scope bar_scope. one looks for notations first in scope bar_scope, then try to use foo, they try for notations in scope foo_scope. - We seize the opportunity of this commit to simplify availability_of_notation which is now integrated to uninterp_notation and which does not have to be called explicitly anymore.
2018-12-04Selecting which notation to print based on current stack of scope.Hugo Herbelin
See discussion on coq-club starting on 23 August 2016.
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
backticks; try to fix all misuses.
2018-12-03[sphinx] Same rendering for :n:`@token` and :token:`token`.Théo Zimmermann
Co-authored-by: Clément Pit-Claudel <clement.pitclaudel@live.com>
2018-12-03A few fixes of unexisting tokens.Théo Zimmermann
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try ↵Théo Zimmermann
to fix all misuses.
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-30Merge PR #9068: [dune] Minor tweak of dependencies.Théo Zimmermann
2018-11-30[gitlab-ci] Increase git depth.Théo Zimmermann
To avoid massive failures in second stage of CI build when a new PR has been merged in master since then. Example: https://gitlab.com/coq/coq/pipelines/38528858.
2018-11-30Merge PR #8807: Added two proofs to the Lists library: Forall_inv_tail and ↵Pierre-Marie Pédrot
Exists_impl
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
And a few more Sphinx fixes in passing.
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
As per https://github.com/coq/coq/pull/8965#discussion_r237225852
2018-11-28Merge PR #9070: [ssreflect] Export more parsing witnesses.Enrico Tassi
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 ↵Michael Soegtrop
enabled_all_addons.
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
Co-authored-by: Michael Soegtrop <michael.soegtrop@intel.com>
2018-11-28coqide: Remove unused win32_kill C functionGaëtan Gilbert
Unused since b0da879dc6abfca6b4e233b7469265a5cf52ce15 (see also followup 4f554c88aa).
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 ↵Pierre-Marie Pédrot
reference.
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 ↵llee454@gmail.com
Forall_inv to assert that a property that is true for every element of a list is true for every element in the tail of the list. The second, Exists_impl, parallels Forall_impl and proves that if there exists an element in a list that satisfies a given predicate, and the predicate implies another proposition, then there exists an element in the list that satisfies the implied proposition. Both of these proofs fill natural gaps within the List library.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:14:41 +0000