From e3d808c4aa7387a12aee0d30a64ea85550b82eb8 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 21 Mar 2013 15:27:15 +0000
Subject: Check unexpected "Local" keyword in cmd before opening a proof (fix
 #2975)

 This fix isn't ideal. Instead, something like States.with_heavy_rollback
 should be able to cancel a proof started during a command interp that failed.
 But anyway, "le mieux est l'ennemi du bien"...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16333 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 1 +
 1 file changed, 1 insertion(+)

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 ()
 
-- 
cgit v1.2.3