| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
Now that `MutualEntry` provides a more uniform interface we can reuse
`Info.t`
In the medium term we shall consolidate `Proof` / `Proof_global` and
`Lemmas` so admitted / finish are uniform too.
|
|
In preparation for the introduction of an opaque mutual definition
type at the `Declare` level we remove the not very useful wrapper
`declare_fix`.
Now we should be ready to profit from `DeclareDef` and its handling of
common stuff such as `restrict_universe_context` and `check_univ_decl`
etc...
|
|
We split the paths for mutual / non-mutual constants, and we enforce
some further invariants, in particular we avoid messing around with
the body of saved constants, and using the indirect accessor.
This should be almost semantically equivalent to the previous code,
including some questionable choices present there.
In further cleanups we will move this code to Declare, which should
hopefully help clarify some of the semantics.
|
|
As suggested by Gaëtan in review, we move declaration of universe
binders to the common code in `DeclareDef`; this changes the semantics
for the assumption case when Recthms is not empty.
|
|
We move towards more unification in the proof save path of interactive
and non-interactive proofs.
|
|
|
|
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
For an inductive block to be template, all its components must also
be. This is probably fixing a few soundness bugs in the process, but I
do not want to think too much about it.
|
|
We also factorize a few checks by returning an option when looking for
a potentially template universe.
|
|
Cleanup: IMHO most of the re-raises here are not worth it.
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
|
|
This PR refactors the handling of ML loadpaths to get it closer to
what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does.
This is motivated as I am leaning toward letting the standard OCaml
machinery handle OCaml includes; this has several benefits [for
example plugins become regular OCaml libs] It will also help in
improving dependency handling in plugin dynload.
The main change is that "recursive" ML loadpaths are no longer
supported, so Coq's `-I` option becomes closer to OCaml's semantics.
We still allow `-Q` to extend the OCaml path recursively, but this may
become deprecated in the future if we decide to install the ML parts
of plugins in the standard OCaml location.
Due to this `Loadpath` still hooks into `Mltop`, but other than that
`.v` location handling is actually very close to become fully
independent of Coq [thus it can be used in other tools such coqdep,
the build system, etc...]
In terms of vernaculars the changes are:
- The `Add Rec ML Path` command has been removed,
- The `Add Loadpath "foo".` has been removed. We now require that the
form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used.
We did modify `fake_ide` as not to add a directory with the empty
`Prefix`, which was not used. This exposed some bugs in the
implementation of the document model, which relied on having an
initial sentence; we have workarounded them just by adding a dummy one
in the two relevant cases.
|
|
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`.
|
|
|
|
|
|
|
|
We restrict hints to be global references, so as to further simplify the
implementation. Allowing arbitrary terms makes it difficult or expensive
to handle properly some actions like universe contexts or hint equality.
Ultimately, the IsConstr constructor for hints should also be removed.
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: ejgallego
|
|
option
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.
We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
|
|
|
|
|
|
|
|
They were already deprecated in two major releases.
|
|
Inductive foo := Bar |. was accepted but it shouldn't have.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
The import of the format should not be done if i<>1 in open_notation.
|
|
|
|
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).
|
|
The "Any" case was not reached formerly for ETPattern and ETConstr as
far as I can see. So there should be no change of semantics.
|
|
reserve parsing keywords
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
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.
|
|
In particular, this fixes #9741.
|
