[plugin] Remove LocalityFixme über hack.

To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.

This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.

1 files changed, 21 insertions, 6 deletions

diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 91abe1019..ea1808a25 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -243,22 +243,37 @@ VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
       [ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
 END
 
-VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ]
+     [ fun ~atts ~st -> let open Vernacinterp in
+         add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
+         st
+     ]
   | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [  add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ]
+     [ fun ~atts ~st -> let open Vernacinterp in
+         add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
+         st
+     ]
   | [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ]
-    -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ]
+    -> [ fun ~atts ~st -> let open Vernacinterp in
+           add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n;
+           st
+       ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
-    -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ]
+    -> [ fun ~atts ~st -> let open Vernacinterp in
+           add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n;
+           st
+       ]
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
-    -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ]
+    -> [ fun ~atts ~st -> let open Vernacinterp in
+           add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
+           st
+       ]
 END
 
 TACTIC EXTEND setoid_symmetry