| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
subsequent work.
Reviewed-by: maximedenes
|
|
courtesy)
- index errors (negative or out of bounds) generally throw (panic)
- hd, last, find backtrack, because here backtracking can actually be useful
added a _throw variant to these functions which panics
This emaphasizes the difference between backtracking and throwing exceptions, which doesn't exist in OCaml.
- simplified the implementation of for_all2 and exist2 (ok, that is a matter of taste ...)
- added assertions which combine a boolean match with a throw.
This makes the code more readable and makes it easier to have more specific error messages.
- added a lastn function
- gave Out_of_bounds a message argument (there is no good reason why invalid_argument has one and this not)
All other exceptions without message argument are quite specific to certain functions (like Not_Found)
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: cpitclaudel
|
|
This allows to refer to them from other part of the manual without any ambiguity.
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: cpitclaudel
|
|
From the CHANGES file in branch v8.9.
|
|
|
|
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: vbgl
|
|
CoqIDE.
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.
|
|
Reviewed-by: Zimmi48
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
This also makes vernacentries correct wrt update_global_env.
|
|
Reviewed-by: gares
|
|
|
|
|
|
|
|
We move the role data into the evarmap instead.
|
|
Reviewed-by: ejgallego
|
|
- Switch gtksourceview to 3.24.11
- Add appropriate set of icons and some other files GTK3 requires
- Add fix for ocamldebug so that this can be debugged
|
|
Preparing for it to be stored in an Environ.env.
|
|
|
|
The stm.ml changes show that for the other classifications either the
vernac_when was ignored, or there was an assert on it forcing it to be
Now or Later depending on the vernac_type.
One may also note that the classification used in top_printers
`VtQuery,VtNow` would have failed those asserts...
|
|
This replaces the mismatched context error, which occurred when
Instance := {} was used with strictly more fields than declared.
Since we later check that field names match those declared for the
instance, now that we reject duplicates we know that there are no
extra fields.
|
|
After removing `Instance : !type` implicit_application is only used in
constrintern. We propagate constant arguments ?allow_partial and
combine_params_freevar.
Also remove unused functions.
|
|
|
|
Closes #10353
May be blocked on #10352
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
We rename modify to map [more in line with the rest of the system] and
make the endline function specific, as it is only used in one case.
|
|
We refactor the terminator API to make it more internal. Indeed we
remove `set_terminator` and `get_terminator` is only there due to
access to internals in the STM `save_proof` path by the infamous
`?proof` parameter.
After this only 2 non-standard terminators remain: obligations and
derive. We will refactor those in next PRs.
|
|
The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.
This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.
Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.
As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.
We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.
|
|
Reviewed-by: aspiwack
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
vernac syntax
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Ack-by: herbelin
|
