diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9329ab9ff3..e8fef00609 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -447,6 +447,7 @@ let vernac_notation = Metasyntax.add_notation (* Gallina *) let start_proof_and_print k l hook = + Locality.check_locality (); (* early check, cf #2975 *) start_proof_com k l hook; print_subgoals () |