| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
"where"-based notation
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
constants.
Reviewed-by: herbelin
|
|
We refactor handling of `-boot` so the "coqlib" guessing routine,
`Envars.coqlib ()` is not called when bootstrapping.
In compositional builds involving Coq's prelude we don't want for this
guessing to happen, as the heuristics to locate the prelude will fail
due to different build layout choices.
Thus after this patch Coq does not do any guessing when `-boot` is
passed, leaving the location of libraries to the usual command line
parameters.
Note that some other tooling still calls `Envars.coqlib`, however this
should happen late enough as for it to be safe; we will fix that
eventually when we consolidate the library for library handling among
tools.
Ideally, we would also remove `Envars.coqlib` altogether, as we want
to avoid clients accessing the Coq filesystem in a non-controlled way.
|
|
Reviewed-by: vbgl
|
|
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
|
|
|
|
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.
|
|
`plugins` needs to be present to coq_makefile variables are properly
initialized.
|
|
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`.
|
|
- zify_iter_specs is entirely in OCaml
- zify_op has been improved
* The generation of proof-terms is more direct
* It does not `rewrite` but instead either performs
a `pose proof` or a `change`
* The support for `and`, `or`, `not`, arrow is hardcoded
* Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x
- zify_elim_let is entirely in OCaml (no Ltac callback)
[micromega] fix stack overflow
Less naive computation of bounds (online elimination of duplicates)
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
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".
|
|
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
building votour
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: ejgallego
|
|
|
|
|
|
They were in Ltac2, but they are of general interest
|
|
|
|
|
|
|
|
Fixes #11726
|
|
|
|
In case no eliminator is given, we wait until `get_eliminator` to
produce the actual eliminator. Using the sigma produced by guess_elim
here would insert an unused universe for the predicate's type in the
sigma.
|
|
We provide the closure of the dependencies manually.
This is still a hack, but not so bad given that the `source`'d files
still do contain that duplication too.
Dune should provide this functionality so we can replace both this
rule and the source files. Actually, that's not hard to implement,
`utop` already supports a printer attribute so these are loaded
automatically, so the ocamldebug mode could do the same.
Should fix #11716
|
|
Reviewed-by: cpitclaudel
|
|
The previous code was only doing that when either in debug or toplevel mode.
Unfortunately, when dealing with open modules the constants might not have
been registered yet, leading to printing failure. I do not see a reason
why this code should fail when used with globals without a user facing name
when the only goal is to compute a set of identifiers that might clash. Thus,
the above failsafe behaviour is now systematic.
Fixes #8206: Module signature error sometimes prints ??.
|
|
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
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.
|
|
|
|
Fixes #11608.
This means -vos doesn't skip proofs for definitions that end with Qed
but don't include Proof and rely on a Set Default Proof Using. However,
this fixes the bug where this pattern would instead hang, due to #11564.
|
|
|
|
|
