diff options
| author | Matthieu Sozeau | 2013-12-11 17:19:01 +0000 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:57 +0200 |
| commit | 55e62174683f293c8f966d8bd486fcb511f66221 (patch) | |
| tree | 461eb0ba28e62fc3be16f77a982bee7a55dfca02 /toplevel | |
| parent | edb73502de9c3c51fb59e57747398e7fe5e391a6 (diff) | |
- Fix handling of polymorphic inductive elimination schemes.
- Avoid generation of dummy universes for unsafe_global*
- Handle side effects better for polymorphic definitions.
Conflicts:
kernel/term_typing.ml
tactics/tactics.ml
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 450b6ee51f..bb702f79f7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1838,7 +1838,8 @@ let check_vernac_supports_locality c l = | VernacSetOpacity _ | VernacSetStrategy _ | VernacSetOption _ | VernacUnsetOption _ | VernacDeclareReduction _ - | VernacExtend _ ) -> () + | VernacExtend _ + | VernacInductive _) -> () | Some _, _ -> Errors.error "This command does not support Locality" (* Vernaculars that take a polymorphism flag *) |