| Age | Commit message (Collapse) | Author |
|---|
|
|
|
As suggested by @psteckler.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also giving the proper local flag to the hint registration, even on a
Global instance, since the instance discharge manage itself the
redefinition of a hint.
|
|
with make -j4
|
|
This is only a partial merge, we stick with using the standard OCaml
(un)capitalize functions.
|
|
Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_.
We take this constraint into account in tools manipulating Ocaml file
names.
|
|
I.e., do not set local flag to false when in a section since
compatibility tells discharge of hints is not supported.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also fixing a bug of get_next_hyp_position when the hypothesis is the
oldest of the context (see test in ltac.v).
|
|
It allows in particular to have "Info" on tactic "assert" and
derivatives not to give an "<unknown>".
|
|
"tactics.ml".
This is in preparation of move of "assert" from old to new proof engine.
|
|
|
|
|
|
`VernacStartTheoremProof`
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fix suggested by Hugo.
|
|
|
|
|
|
|
|
|
|
The status of a warning can now be set before the warning is declared
(typically by a plugin). However, I had to remove the "unknown warning"
warning.
|
|
Pointed out by PMP.
|
|
|
