| Age | Commit message (Collapse) | Author |
|---|
|
This is to avoid depending on the combination "Discharge" + no opened
section to trigger an automatic declaration of instance.
|
|
Reviewed-by: ejgallego
Ack-by: gares
|
|
Type's argument
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
AFAICT the stm never gives Load a non-None ?proof.
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
|
|
This provides uniformity to the inner loop and prepares the way to
export a refined type for interpretation.
The only non-uniformity remaining is the one due to the `?proof`
parameter; it won't be easy to fix due to upper layers issues.
Note that this step is not yet fully satisfying, as a true typed
`vernac_expr` definition is still not possible because of syntactic
non-uniformity, in particular all the surgery done for `CoFixpoint`
and `Instance` should be eliminated in favor of more refined AST tags.
An interesting TODO is to handle attributes symbolically too, as to
remove boilerplate.
|
|
Reviewed-by: mattam82
|
|
deprecated attribute
This code was significantly more complex than necessary.
|
|
|
|
|
|
|
|
|
|
+ hide interp_functional_vernac in vernacentries
|
|
The only use of ModifyProofStack was in paramcoq for closing a proof.
|
|
|
|
|
|
|
|
eg ![proof] becomes STATE proof
This commits still supports the old ![]
so there is redundancy:
~~~
VERNAC EXTEND Foo STATE proof
| ...
VERNAC EXTEND Foo
| ![proof] ...
~~~
with the ![] form being local to the rule and the STATE form
applying to the whole EXTEND except for the rules with a ![].
|
|
![proof_stack] is equivalent to the old meaning of ![proof]: the body
has type `pstate:Proof_global.t option -> Proof_global.t option`
The other specifiers are for the following body types:
~~~
![open_proof] `is_ontop:bool -> pstate`
![maybe_open_proof] `is_ontop:bool -> pstate option`
![proof] `pstate:pstate -> pstate`
![proof_opt_query] `pstate:pstate option -> unit`
![proof_query] `pstate:pstate -> unit`
~~~
The `is_ontop` is only used for the warning message when declaring a
section variable inside a proof, we could also just stop warning.
The specifiers look closely related to stm classifiers, but currently
they're unconnected. Notably this means that a ![proof_query] doesn't
have to be classified QUERY.
![proof_stack] is only used by g_rewrite/rewrite whose behaviour I
don't fully understand, maybe we can drop it in the future.
For compat we may want to consider keeping ![proof] with its old
meaning and using some new name for the new meaning. OTOH fixing
plugins to be stricter is easier if we change it as the errors tell us
where it's used.
|
|
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
|
|
Not needed since we don't allow anonymous Declare Instance
anymore (was needed for factorization or some such before that I think)
|
|
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
|
|
We consistently use:
- UUnknown: to mean a rigid anonymous universe
(written Type in instances and Type as a sort)
[was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
(written _ in instances and Type@{_} as a sort)
[was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
(written id or qualid in instances and Type@{id} or Type@{qualid} or more
generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)
There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.
There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.
|
|
|
|
This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.
The syntax is: `Arguments foo x y | z`.
Closes #7910
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
We get rid of the future wrappers, as all callers are immediately forcing
the result.
|
|
Reviewed-by: Zimmi48
|
|
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.
|
|
|
|
* 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.
|
|
vernac
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: vbgl
|
|
|
|
|
|
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 .
|
|
This lets us avoid passing ~ontop to do_definition and co, and after #10050
to even more functions.
|
|
It's used a few times in the stdlib (a couple of which need no other
change when removing the !) and not at all throughout our CI.
Considering that I think it's fair enough to remove it.
|
|
This code was originally part of #8811, authored by Gaëtan Gilbert.
It seems we are not very consistent on what we do when we use
`ParameterEntry`, specially w.r.t. universes but as code cleanup
progresses we will have a better view.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.
The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.
We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.
Fixes #3632 #3890 #4638.
|
|
|
|
Not sure why we didn't. Fail didn't catch anomalies almost by accident.
It still makes sense to catch Timeout here imo
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
