| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
|
|
a context.
Reviewed-by: mattam82
|
|
|
|
|
|
|
|
- take just a ugraph instead of the whole env
- rename to update_sigma_univs
- push global env lookup a bit further up
- fix vernacinterp call to update all surrounding proofs, not just the
top one
- flip argument order for nicer partial applications
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
|
|
|
|
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml
library which is a more modern version.
We switch the core files and easy plugins only for now, more complex
numerical plugins will be done in their own commit.
We thus keep the num library linked for now until all plugins are
ported.
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Ack-by: Zimmi48
Reviewed-by: anton-trunov
|
|
Added user overlay for bignums
|
|
recognition.
Reviewed-by: mattam82
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
|
|
|
|
|
|
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
Indeed, it would be intuitive that `Require Import Ltac` is an
equivalent for Ltac of `Require Import Ltac2.Ltac2`.
Also declaring the classic proof mode.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
|
|
|
|
|
|
- problem with metacoq overlay ; it expects to send a non-ground
constant to the kernel, now it fails at prepare.
Record Sigma (A : Type) (B : A -> Type) : Type :=
{ fst : A ; snd : B fst }.
Arguments fst {A B}.
Arguments snd {A B}.
Quote Recursively Definition foo := (fst, snd).
There is a hack on the overlay, we need to discuss it a bit more.
|
