diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-24 12:46:57 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-24 12:46:57 +0100 |
| commit | 31794a1828a15acb95c235fd3166c511635add41 (patch) | |
| tree | fb09a6b201001ababc3030dc80fa9d729526c0a7 /vernac/vernacentries.ml | |
| parent | 92c15a9b660b874ce3fa125b1f9bdf2e85c40f47 (diff) | |
| parent | 57f62f06419972ba799e451d2f56552dc1b2fb63 (diff) | |
Merge PR #6197: [plugin] Remove LocalityFixme über hack.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6191f3708..62c7edb19 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2078,7 +2078,7 @@ let interp ?proof ?loc locality poly st c = (* Extensions *) | VernacExtend (opn,args) -> (* XXX: Here we are returning the state! :) *) - let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in + let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) ~st in () (* Vernaculars that take a locality flag *) |