diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4c12b4e7b..b6e625136 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1626,7 +1626,7 @@ let interp c = Flags.program_cmd := false; Obligations.set_program_mode isprogcmd; try - interp c; check_locality (); + interp c; Locality.check_locality (); Flags.program_mode := mode with e -> Flags.program_mode := mode; |