| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
This was dead code.
|
|
This is actually dead code, we never observe it.
|
|
This is just moving code around, so it should not change the semantics.
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
The current situation is a mess, some functions set it by default, but other
no. Making it mandatory ensures that the expected value is the correct one.
|
|
This prevents having to call global functions, for no good reason.
We also seize the opportunity to name the check argument.
|
|
Some of them are significant so presumably it will take a bit of
effort to fix overlays.
I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
|
|
Reviewed-by: ppedrot
|
|
as assumptions
Ack-by: RalfJung
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: maximedenes
Reviewed-by: ppedrot
Ack-by: robbertkrebbers
|
|
(Merge of the initial version with #9983 was broken)
|
|
We add a fast path when generalizing over variables.
|
|
|
|
The creation of the local hint db now inherits the union of the modes
from the dbs passed to `typeclasses eauto`.
We could probably go further and define in a more systematic way the
metadata that should be inherited. A lot of this code could also be
cleaned-up by defining the merge of databases, so that the search code
is parametrized by just one db (the merge of the input ones).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
already there.
Reviewed-by: gares
|
|
|
|
|
|
I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.
|
|
One other call still remains, but will require to refactor some
section-handling code.
|
|
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
|
|
State in `Proof_global` was mostly used for debugging, so not a big
change.
|
|
|
|
This is an experimental PR as I am not sure I can follow the reasoning
in e1ba72037191b1d4be9de8a0a8fc1faa24eeb12c
Note that in safe_typing we avoid re-declaring effects twice.
This removes a huge number of redeclaration of schemes side-effects
that in fact are already generated such as `eq_ind`.
Anyways we should deprecate the declaration of Schemes on-the-fly, I
don't see the point honestly; just make sure your theory has the right
ones.
Well, going to a more eager declaration scheme could be costly in
terms of size, so OMMV.
TODO: only declare side-effects if the scheme is generated on-the-fly,
add a parameter to the declaration function.
|
|
Previously, they were hard-wired in the ML code.
|
|
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
Ack-by: gares
Ack-by: herbelin
Ack-by: mattam82
Ack-by: ppedrot
|
|
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
|
|
I think the usage looks cleaner this way.
|
|
In order to do so we place the polymorphic status and name in the
read-only part of the monad.
Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.
Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.
Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.
|
|
Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).
Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).
|
