| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
This fixes #11547 ; note that it is hard to register such handlers in
the `Summary` due to layering issues; there are potential anomalies here
depending on how plugins do register their data structures.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
This is to be consistent with "pose (x:=a)" (and an alternative to
"assert (x:=a)").
This was suggested by
"https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962".
|
|
|
|
|
|
It was not documented, I do not think it is used in the wild, and it relies
on legacy code. As solid conjunction of reasons that support its deprecation.
|
|
argument
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
This was redundant with `iraise`; exceptions in the logic monad now
are forced to attach `info` to `Proofview.NonLogical.raise`
|
|
"refresh" argument
Reviewed-by: ppedrot
|
|
Also renamed it to relative_entry_level.
Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused
Should not change global semantics (except error message in pr_arg).
|
|
This PR is in preparation of #9067 (together with #11647) .
Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.
|
|
It's been ignored since the introduction of universe polymorphism.
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Instead of various termops and globnames aliases.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional
environment instead of querying the imperative global one. We percolate
this change as higher up as possible.
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
|
|
Some calls are actually guarded by a check that the scheme is already in
the cache. There is no reason to generate dummy side-effects in that case.
|
|
Fixes #10971
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Failing on CProdN([],...) was maybe a bit too radical.
|
|
Reviewed-by: ppedrot
|
|
The manual was already saying that it was deprecated, but no warning was
emitted.
Fixes #10572
|
|
This lets us get rid of dummy proofview manips.
Simplifications based on [(tclUNIT foo >>= f) = f foo]
|
|
The proposed replacements are not satisfying because they are more
complicated to use. Following the discussion in #8713, we decide to
remove the deprecation warning for these commands.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
We can now do `#[refine] Instance : Bla := bli.` to enter proof mode
with `bli` as a starting refinement.
If `bli` is enough to define the instance we still enter proof mode,
keeping things nicely predictable for the stm.
|
|
|
|
#10239).
The bug was introduced in #10239 which seems to have actually remained
half-done: "wit_intropattern" and "wit_simple_intropattern" did not
share the same representation of values (val_tag) but the code was
assuming (especially the code for "fresh") that this was shared.
We fix it by sharing the internal representation (`dyn` field in
Tacarg.make0) as suggested by @ppedrot in the discussion of #10239
(this allows also to simplify Taccoerce.is_intro_pattern).
|
|
As documented in the feedback API.
|
|
|
|
Reviewed-by: SkySkimmer
|
