| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
|
|
This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.
The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
|
|
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
|
|
We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.
|
|
|
|
|
|
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
|
|
Most functions are taken either from the Coq standard library or the
OCaml standard library. One (`enumerate`) is taken from Python. Most
names are chosen according to OCaml conventions (as Coq does not have
exceptions, and so the OCaml naming conventions already distinguish
between option and exception). Since `exists` is a keyword, we use the
Coq name `existsb` instead. We generally favor Coq argument ordering
when there is a conflict between Coq and OCaml.
Note that `seq` matches neither Coq nor OCaml; it takes a `step`
argument for how much to increment by on each step.
Sorting functions are mostly taken from Coq's mergesort library; it
might make sense to replace them with OCaml's versions for efficiency?
|
|
|
|
|
|
|
|
|
|
|
|
- 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
|
|
|
|
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
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
|
