| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: cpitclaudel
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ggonthier
Reviewed-by: herbelin
Ack-by: jfehrle
Reviewed-by: mattam82
|
|
We list preexisting undefined tokens explicitly in
`doc/sphinx/conf.py` and prevent new ones from being introduced by
making it a fatal warning.
This list should be seen as a TODO. Once it is emptied, #9411 can be
closed.
|
|
Reviewed-by: cpitclaudel
Reviewed-by: ppedrot
|
|
Ack-by: JasonGross
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
binding semantics.
Ack-by: Zimmi48
|
|
* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.
|
|
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
vernac
Reviewed-by: maximedenes
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
|
|
3d09e39dd423d81c6af3e991d5b282ea8608646b
The commit mentioned above changed the semantics of `Bind Scope` to
a dynamic binding behavior. It forgot to update the documentation.
Fixes #10064
|
|
|
|
Ack-by: Zimmi48
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: vbgl
|
|
Reviewed-by: gares
|
|
|
|
|
|
|
|
|
|
|
|
- use coqc instead of coqtop (since -compile doesn't work anymore this
is better)
- pass through extra arguments to dune-dbg
- auto detect the need to pass -emacs to ocamldebug
- instructions for emacs users
The dune-dbg dependencies are still broken ;_;
|
|
|
|
Co-Authored-By: @Zimmi48
|
|
|
|
generalization + cleanups
Reviewed-by: herbelin
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: gares
Reviewed-by: jfehrle
Reviewed-by: vbgl
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: SkySkimmer
|
|
Typeclasses resolution is not used anymore for lia.
Typeclasses resolution is still used by lra but only to access a
database of declared constants.
|
|
|
|
|
|
Closes #8735 .
|
|
|
|
We cleanup a bit the implementation of LoadPath which is not possible
as now all the loadpath logic is in the same place.
In particular, we remove exceptions in favor a `locate_result` monad.
More cleanup should still be possible, in particular
`locate_absolute_library` and `locate_qualified_library` should be
merged.
|
|
We consolidate loadpath handling as a single `Loadpath` module from
parts in `Library` and `Mltop`, placing it at the `vernac` level [as
`Mltop`]
This idea was first suggested in https://github.com/coq/coq/pull/9808
, and indeed it makes sense as library resolution tends to be business
of the upper layers: IDE / build tools.
Logic could be pushed upwards, but this is good enough for now.
This consolidation has enabled some good and long overdue
refactorings, and the module should become self-contained enough as to
allow the resolution logic to be shared with `coqdep` in the future.
The `Mltop` module only cares now about ML-level modules, and should
go away once we rewrite the loader using `findlib` to solve
https://github.com/coq/coq/issues/7698 .
|
|
Reviewed-by: gares
|
|
Ack-by: gares
Ack-by: herbelin
Reviewed-by: vbgl
|
|
|
|
This lets us avoid passing ~ontop to do_definition and co, and after #10050
to even more functions.
|
