Vernac classification streamlined (handles VERNAC EXTEND)

The warning output by vernacextend when the classifier is missing
is the documentation of this commit:

Warning: Vernac entry "Foo" misses a classifier. A classifier is a
function that returns an expression of type vernac_classification (see
Vernacexpr). You can:
- Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new
  vernacular command does not alter the system state;
- Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new
  vernacular command alters the system state but not the parser nor it starts
  a proof or ends one;
- Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global
  function f.  The function f will be called passing "Foo" as the
  only argument;
- Add a specific classifier in each clause using the syntax:
  '[...] => [ f ] -> [...]'.
Specific classifiers have precedence over global classifiers. Only one
classifier is called.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 46 insertions, 34 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 21678c9714..646c57d95f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -735,12 +735,12 @@ let set_transparency cl b =
     let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in
       Classes.set_typeclass_transparency ev false b) cl
 
-VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
+VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
 | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
     set_transparency cl true ]
 END
 
-VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
+VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
 | [ "Typeclasses" "Opaque" reference_list(cl) ] -> [
     set_transparency cl false ]
 END
@@ -765,7 +765,7 @@ END
 
 (* true = All transparent, false = Opaque if possible *)
 
-VERNAC COMMAND EXTEND Typeclasses_Settings
+VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
  | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [
      set_typeclasses_debug d;
      set_typeclasses_depth depth
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 713d6f233a..6b607c38d2 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -600,7 +600,7 @@ ARGUMENT EXTEND opthints
 | [ ] -> [ None ]
 END
 
-VERNAC COMMAND EXTEND HintCut
+VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
 | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
   let entry = HintsCutEntry p in
     Auto.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ae617a4d8a..a935f69002 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -259,7 +259,9 @@ let add_rewrite_hint bases ort t lcsr =
   let add_hints base = add_rew_rules base eqs in
   List.iter add_hints bases
 
-VERNAC COMMAND EXTEND HintRewrite
+let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater
+
+VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY classify_hint
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
   [ add_rewrite_hint bl o None l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
@@ -300,14 +302,14 @@ let add_hints_iff l2r lc n bl =
   Auto.add_hints true bl
     (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc))
 
-VERNAC COMMAND EXTEND HintResolveIffLR
+VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
   [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
   [ add_hints_iff true lc n bl ]
 | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
   [ add_hints_iff true lc n ["core"] ]
 END
-VERNAC COMMAND EXTEND HintResolveIffRL
+VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
   [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
   [ add_hints_iff false lc n bl ]
@@ -332,17 +334,20 @@ let refine_tac = refine
 open Inv
 open Leminv
 
+let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
+
 VERNAC COMMAND EXTEND DeriveInversionClear
-  [ "Derive" "Inversion_clear" ident(na) hyp(id) ]
+  [ "Derive" "Inversion_clear" ident(na) hyp(id) ] => [ seff na ]
   -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_clear_tac ]
 
-| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ]
+| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ] => [ seff na ]
   -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
+  => [ seff na ]
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
-| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ]
+| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ]
   -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ]
 END
 
@@ -350,25 +355,28 @@ open Term
 
 VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
+  => [ seff na ]
   -> [ add_inversion_lemma_exn na c s false inv_tac ]
 
-| [ "Derive" "Inversion" ident(na) "with" constr(c) ]
+| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ]
   -> [ add_inversion_lemma_exn na c GProp false inv_tac ]
 
-| [ "Derive" "Inversion" ident(na) hyp(id) ]
+| [ "Derive" "Inversion" ident(na) hyp(id) ] => [ seff na ]
   -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ]
 
-| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ]
+| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ] => [ seff na ]
   -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
 | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
+  => [ seff na ]
   -> [ add_inversion_lemma_exn na c s true dinv_tac ]
-    END
+END
 
 VERNAC COMMAND EXTEND DeriveDependentInversionClear
 | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
+  => [ seff na ]
   -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
 END
 
@@ -470,17 +478,17 @@ TACTIC EXTEND stepr
 | ["stepr" constr(c) ] -> [ step false c tclIDTAC ]
 END
 
-VERNAC COMMAND EXTEND AddStepl
+VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF
 | [ "Declare" "Left" "Step" constr(t) ] ->
     [ add_transitivity_lemma true t ]
 END
 
-VERNAC COMMAND EXTEND AddStepr
+VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF
 | [ "Declare" "Right" "Step" constr(t) ] ->
     [ add_transitivity_lemma false t ]
 END
 
-VERNAC COMMAND EXTEND ImplicitTactic
+VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF
 | [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
     [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ]
 END
@@ -491,7 +499,7 @@ END
 (**********************************************************************)
 (*spiwack : Vernac commands for retroknowledge                        *)
 
-VERNAC COMMAND EXTEND RetroknowledgeRegister
+VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
  | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
            [ let tc = Constrintern.interp_constr Evd.empty (Global.env ()) c in
              let tb = Constrintern.interp_constr Evd.empty (Global.env ()) b in
@@ -766,7 +774,7 @@ END;;
    the semantics of the LCF-style tactics, hence with the classic tactic
    mode. *)
 VERNAC COMMAND EXTEND GrabEvars
-[ "Grab" "Existential" "Variables" ] ->
-  [ Proof_global.with_current_proof (fun _ p  ->
-      Proof.V82.grab_evars p) ]
+[ "Grab" "Existential" "Variables" ]
+  => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ]
+  -> [ Proof_global.with_current_proof (fun _ p  -> Proof.V82.grab_evars p) ]
 END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 154cad6913..c855486db4 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1643,7 +1643,7 @@ let wit_binders =
  (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type)
 
 
-VERNAC COMMAND EXTEND AddRelation
+VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
 	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ]
@@ -1655,7 +1655,7 @@ VERNAC COMMAND EXTEND AddRelation
       [ declare_relation a aeq n None None None ]
 END
 
-VERNAC COMMAND EXTEND AddRelation2
+VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
     [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       [ declare_relation a aeq n None (Some lemma2) None ]
@@ -1663,7 +1663,7 @@ VERNAC COMMAND EXTEND AddRelation2
       [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ]
 END
 
-VERNAC COMMAND EXTEND AddRelation3
+VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
     [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ]
@@ -1676,7 +1676,7 @@ VERNAC COMMAND EXTEND AddRelation3
       [ declare_relation a aeq n None None (Some lemma3) ]
 END
 
-VERNAC COMMAND EXTEND AddParametricRelation
+VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
 	"reflexivity" "proved" "by" constr(lemma1)
 	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
@@ -1689,7 +1689,7 @@ VERNAC COMMAND EXTEND AddParametricRelation
       [ declare_relation ~binders:b a aeq n None None None ]
 END
 
-VERNAC COMMAND EXTEND AddParametricRelation2
+VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
     [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n None (Some lemma2) None ]
@@ -1697,7 +1697,7 @@ VERNAC COMMAND EXTEND AddParametricRelation2
       [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ]
 END
 
-VERNAC COMMAND EXTEND AddParametricRelation3
+VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
     [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
       [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ]
@@ -1846,18 +1846,22 @@ let add_morphism glob binders m s n =
     ignore(new_instance ~global:glob binders instance (Some (CRecord (Loc.ghost,None,[])))
 	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
 
-VERNAC COMMAND EXTEND AddSetoid1
+VERNAC COMMAND 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 ]
   | [ "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 ]
-  | [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
-      [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ]
-  | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ]
+  | [ "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 ]
+  | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
+    => [ Vernacexpr.VtStartProof("Classic",[n]), Vernacexpr.VtLater ]
+    -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ]
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
-	"with" "signature" lconstr(s) "as" ident(n) ] ->
-      [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ]
+	"with" "signature" lconstr(s) "as" ident(n) ]
+    => [ Vernacexpr.VtStartProof("Classic",[n]), Vernacexpr.VtLater ]
+    -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ]
 END
 
 (** Bind to "rewrite" too *)