diff options
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 450b6ee51..bb702f79f 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 *) |