diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-31 18:45:41 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-23 18:23:04 +0200 |
commit | 13716dc6561a3379ba130f07ce7ecd1df379475c (patch) | |
tree | bcb347d50031561d16afa8430208d5deaf9cfdf8 /library/library.ml | |
parent | 6459c0e8c240f0997873c50d4ec749effaba2f44 (diff) |
Give a way to control if the decidable-equality schemes are built like
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions