| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-08 | [dune] Install coq libraries in `%{lib_root}/coq` instead of `lib` | Emilio Jesus Gallego Arias | |
| This is what the native Dune Coq version already does, but it is a problem for Coq Dune too as noted by @vgbl. | |||
| 2018-12-07 | Merge PR #8811: EConstr-aware functions to produce kernel entries | Pierre-Marie Pédrot | |
| 2018-12-06 | Merge PR #9140: [ci] Add four color theorem proof to CI | Gaëtan Gilbert | |
| 2018-12-06 | High level functions to produce kernel entries from econstr. | Gaëtan Gilbert | |
| 2018-12-06 | Evarutil.finalize: combine minimize, to_constr and restrict. | Gaëtan Gilbert | |
| 2018-12-06 | Merge PR #8917: Small cleanup wrt attributes_of_flags and template attribute | Vincent Laporte | |
| 2018-12-06 | Merge PR #9069: [gramlib] Remove dead code | Hugo Herbelin | |
| 2018-12-05 | [ci] Add four color theorem proof to CI | Emilio Jesus Gallego Arias | |
| 2018-12-05 | Remove the Like level modifier from gramlib. | Pierre-Marie Pédrot | |
| Apart from the fact we did not use it, its semantics was somewhat flaky as it was looking for any rule containing some token. | |||
| 2018-12-05 | Remove the grammar-entry correspondence dynamic check in camlp5. | Pierre-Marie Pédrot | |
| Due to the fact we only export the functorial API, this property is ensured statically. There is thus no point in checking it. | |||
| 2018-12-05 | Removing dead fields from Plexing.lexer. | Pierre-Marie Pédrot | |
| 2018-12-05 | Remove dead code in camlp5. | Pierre-Marie Pédrot | |
| The references error_verbose and strict_parsing were not accessible from the API, so their value was statically known. | |||
| 2018-12-05 | Remove the lexer field from Gramlib. | Pierre-Marie Pédrot | |
| This is useless in the functorial API. | |||
| 2018-12-05 | Make some camlp5 fields immutable. | Pierre-Marie Pédrot | |
| 2018-12-05 | Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Pierre-Marie Pédrot | |
| 2018-12-05 | Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks. | Pierre-Marie Pédrot | |
| 2018-12-05 | Move template out of Defattributes record | Gaëtan Gilbert | |
| 2018-12-05 | attributes_of_flags and its output type now internal in vernacentries | Gaëtan Gilbert | |
| 2018-12-05 | Merge PR #8911: Document undocumented flags and options | Théo Zimmermann | |
| 2018-12-04 | Add undocumented options from mattam82 | Jim Fehrle | |
| 2018-12-04 | Document undocumented flags and options | Jim Fehrle | |
| Also remove a few undocumented settings | |||
| 2018-12-04 | Remove undocumented "Proof using Clear Unused" flag | Jim Fehrle | |
| 2018-12-04 | Merge PR #9134: CI: track dev branch of coq-simple-io | Emilio Jesus Gallego Arias | |
| 2018-12-04 | CI: track dev branch of coq-simple-io | Yishuai Li | |
| 2018-12-04 | Merge PR #9127: Remove leftover code that used to handle ml4 files. | Emilio Jesus Gallego Arias | |
| 2018-12-04 | Merge PR #8187: Notation printing based on scopes (take 2, including bug fixes) | Emilio Jesus Gallego Arias | |
| 2018-12-04 | Remove leftover code that used to handle ml4 files. | Pierre-Marie Pédrot | |
| 2018-12-04 | Merge PR #9053: Document code owner team creation. | Maxime Dénès | |
| 2018-12-04 | Giving 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-04 | Notation.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-04 | Fixing missing newline in display of Locate for notations. | Hugo Herbelin | |
| 2018-12-04 | Printing 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-04 | Documentation of the rules for printing notations depending on scopes. | Hugo Herbelin | |
| Mostly courtesy of Jason Gross. | |||
| 2018-12-04 | Using scope for printing: more tests. | Hugo Herbelin | |
| 2018-12-04 | Fixing #8551 (missing delimiters when notation exists both lonely and in scope). | Hugo Herbelin | |
| 2018-12-04 | Addressing 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-04 | Selecting which notation to print based on current stack of scope. | Hugo Herbelin | |
| See discussion on coq-club starting on 23 August 2016. | |||
| 2018-12-04 | Pre-isolating a notation test to avoid interferences. | Hugo Herbelin | |
| 2018-12-03 | Merge 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-03 | A few fixes of unexisting tokens. | Théo Zimmermann | |
| 2018-12-03 | Closes #9118: single backticks are made equivalent to double backticks; try ↵ | Théo Zimmermann | |
| to fix all misuses. | |||
| 2018-12-03 | Merge PR #9119: [gitlab-ci] Increase git depth. | Gaëtan Gilbert | |
| 2018-12-03 | Merge 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 | |
| We make `declaration_hook`s optional arguments everywhere, and thus we avoid some "fake" functions having to be passed. This identifies positively the code really using hooks [funind, rewrite, coercions, program, and canonicals] and helps moving toward some hope of reification. | |||
| 2018-11-30 | [gramlib] Remove `Ploc.t` in favor of `Loc.t` | Emilio Jesus Gallego Arias | |
| The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option` | |||
| 2018-11-30 | Merge 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-30 | Merge PR #8807: Added two proofs to the Lists library: Forall_inv_tail and ↵ | Pierre-Marie Pédrot | |
| Exists_impl | |||
| 2018-11-30 | Merge PR #9105: Add indexes for coercion / substructure symbol :>. | Clément Pit-Claudel | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |