diff options
| author | Matej Kosik | 2015-12-16 15:50:40 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-18 15:58:43 +0100 |
| commit | 20641795624dbb03da0401e4dc503660e5e73df6 (patch) | |
| tree | 3e4a94692a2c7ec1c722e8a8a3db94783a4cd684 /pretyping/typeclasses_errors.ml | |
| parent | 84f54fd0923c15109910123443348c193e37fe0f (diff) | |
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions