diff options
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 10c139e5a..358e965ec 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 *) |