| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Instead of setting globally the option, we add a hook to set it in
the init object of the plugin.
|
|
|
|
|
|
|
|
|
|
`Require`.
|
|
|
|
constructor it is.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This prevents careless confusions with generic arguments from Coq.
|
|
This is a way to hack around the fact that various interpretation functions
rely wrongly on the values of the environment to do nasty tricks. Typically,
the interpretation of terms is broken, as it will fail when there is a bound
variable with the same name as a hypothesis, instead of producing the
hypothesis itself.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This is for backward compatibility.
|
|
|
|
|
