| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
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.
|
|
This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
local fix/cofix (#10197)
Reviewed-by: maximedenes
|
|
#10205.
Reviewed-by: cpitclaudel
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: cpitclaudel
|
|
|
|
These were found with the following command:
$ git grep "1999-" | grep -v "2019"
|
|
Remove mentions of removed plugins.
Remove copyright years to avoid them going out of sync.
Fix explanation of the license of the documentation.
|
|
Remove other types of lines before copyright headers.
|
|
Most of these files were introduced after #6543 but used older headers
copied from somewhere else.
|
|
|
|
|
|
|
|
ml-style headers.
|
|
|
|
|
|
This enforces more invariants statically.
|
|
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
|
|
Reviewed-by: herbelin
|
|
works on MacOS X
Reviewed-by: SkySkimmer
|
|
Works fine here, cc: #9975
|
|
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: tlringer
|
|
|
|
|
|
Small refactoring to pass the `sigma` functionally.
|
|
Equation's terminator had exactly duplicated the shrink function used
in `Abstract`, we remove this duplicity.
|
|
We add the and routine the regular proof save path of Equations was
using.
I don't understand what is going on here, these are a few remarks:
- Equations does capture `sigma` at the time of `start_dependent_lemma`
- A custom hook is also captured, along with telescopes
- The shrink function seems like a duplicate with things already in Coq's
[abstract.ml / declareObl.ml]
I guess the preferred option would be to merge this with the
obligations save path; but I need help from experts.
|
|
Just a cleanup, should bring no functional code change.
|
|
We radically redesign how proof closing information is stored. Instead
of a user-defined closure, we now reify control into a single data
structure containing the needed information.
In this scheme, the `Lemmas` module can get extra information with
obligation info when opening the proof, and will correspondingly call
the right closing function based on this.
This is the start of what could be a much bigger unification of all
the proof save paths.
|
|
This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.
|
|
This makes the type of terminator simpler, progressing towards its
total reification.
|
|
We move obligation declaration-specific functions to their own
file. This way, `Lemmas` can access them, and in the next part we can
factorize common parts in the save proof.
|
|
As of now, hooks were stored in the terminators as closures, we place
them instead in the proof object and are thus passed back at proof
closing time.
This helps towards the reification and unification of terminators.
|
|
differ in term and type
Reviewed-by: ejgallego
Ack-by: jashug
|
|
Reviewed-by: cpitclaudel
|
|
same thing.
Reviewed-by: ejgallego
|
|
|
|
This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual
After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.
Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.
|
|
Unfortunately, "+" regular expressions are not supported by default
with MacOS X's sed.
It is told that it would work with option -E though, but the syntax
seems then different.
|
|
The ML wrapper was wrongly calling induction instead of destruct.
|
|
Reviewed-by: ejgallego
|
