| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
They were in Ltac2, but they are of general interest
|
|
option
Reviewed-by: ppedrot
|
|
argument
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: tchajed
|
|
This was redundant with `iraise`; exceptions in the logic monad now
are forced to attach `info` to `Proofview.NonLogical.raise`
|
|
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.
|
|
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.
|
|
We use the same kind of trick as the one we used for &IDENT, namely check
that no space appear between the dollar sign and the identifier.
|
|
Actually, callers of the Pvernac.register_proof_mode function have to
manually register the parsing of vernacular queries themselves. This
probably qualifies as an oversight from myself.
|
|
This prevents some warnings to be dropped when the variables are not used at
the right type. See #11603 for a motivation.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
There was an evar leak due to an evarmap not being threaded correctly
when computing open terms.
|
|
|
|
a module
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
|
|
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
|
|
We implement a new type of "preterms" that represent untyped ASTs, corresponding
to glob_expr in the ML implementations. Ltac2 quotations inside notations are
provided with such preterms, and have to pretype them in order to do anything
of relevance with them.
|
|
This is the dual of #10344.
|
|
They probably don't need to be executable
|
|
|
|
|
|
|
|
|
|
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
|
|
This looks more principled, and doesn't require as much tinkering with
the typing implementation.
|
|
|
|
Ack-by: JasonGross
Ack-by: MSoegtropIMC
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
option combinators
|
|
Changed year in headers
|
|
We place the check for unhandled exceptions in the `is_anomaly`
function, and consider all the exceptions non-handled by the printers
always anomalies.
This reworks the solution implemented in
ea3909466eaaf86ff212c0a002e5df11e4a979f5 , in particular
`allow_uncaught` cannot be used anymore, all exceptions must install a
printer.
In order to pass the test-suite CI we also had to register some
printers, that were not registered for no reason, forcing clients to
call a post-processing step on errors.
|
|
Most of these files were introduced after #6543 but used older headers
copied from somewhere else.
|
|
same thing.
Reviewed-by: ejgallego
|
|
The ML wrapper was wrongly calling induction instead of destruct.
|
|
Reviewed-by: ejgallego
|
|
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)
|
|
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...
|
|
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.
|
