aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
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
We remove a few aliases present in the lower layers [`Genintern/Tactypes`] from `Tacexpr`. IMHO this enlarges the API for no good purpose, and difficults analysis.
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
This makes setting the option outside of the synchronized summary impossible.
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
We update the Appveyor configuration so it uses OPAM 2.0, and thus it can install newer packages.
2018-11-27[lib] Remove leftover flag `print_mod_uid`Emilio Jesus Gallego Arias
The whole `native_name_from_filename` business seems quite strange tho.
2018-11-27[gramlib] Remove unused function `gram_reinit`.Emilio Jesus Gallego Arias
2018-11-27[pcoq] Remove a redundant `entry` type.Emilio Jesus Gallego Arias
This was done in a bit of redundant way when we removed the camlp4 compat layer; we fix this and make the type flow clearer.
2018-11-27[gramlib] Minor cleanups:Emilio Jesus Gallego Arias
- remove duplicate type definitions `gram_assoc`, `gram_position`, - make global `warning_verbose` variable into a parameter.
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a ↵Emilio Jesus Gallego Arias
write_function
2018-11-27Make `-async-proofs on` effective with `coqc`Maxime Dénès
Before this patch, it had no effect.
2018-11-27Remove -async-proofs-full flagMaxime Dénès
The semantics of this flag was not clear, it had several rather orthogonal effects. Also, it should probably have been another value of `-async-proofs-mode`, rather than a separate flag, as its combination with e.g. `-async-proofs-mode off` is unclear.
2018-11-27Merge PR #7033: Remove obsolete files from dev/docThéo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:28:23 +0000