Useless use of hooks in VernacDefinition. In addition, this was

polluting the AST first-order structure.

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

4 files changed, 30 insertions, 25 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 52120d73c3..528fd69f30 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -232,11 +232,10 @@ type vernac_expr =
       scope_name option
 
   (* Gallina *)
-  | VernacDefinition of definition_kind * lident * definition_expr *
-      unit declaration_hook
+  | VernacDefinition of definition_kind * lident * definition_expr
   | VernacStartTheoremProof of theorem_kind *
       (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list *
-        bool * unit declaration_hook
+        bool
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index fb5524945d..47d1796ced 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -68,7 +68,6 @@ let default_command_entry =
   Gram.Entry.of_parser "command_entry"
     (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
 
-let no_hook _ _ = ()
 GEXTEND Gram
   GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
   vernac: FIRST
@@ -154,14 +153,14 @@ GEXTEND Gram
         l = LIST0
           [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
             (Some id,(bl,c,None)) ] ->
-          VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook)
+          VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | stre = assumptions_token; nl = inline; bl = assum_list ->
 	  test_plurial_form bl;
 	  VernacAssumption (stre, nl, bl)
-      | (f,d) = def_token; id = identref; b = def_body ->
-          VernacDefinition (d, id, b, f)
+      | d = def_token; id = identref; b = def_body ->
+          VernacDefinition (d, id, b)
       (* Gallina inductive declarations *)
       | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
@@ -197,13 +196,13 @@ GEXTEND Gram
   ;
   def_token:
     [ [ "Definition" ->
-	no_hook, (Global, Definition)
+	(Global, Definition)
       | IDENT "Let" ->
-	no_hook, (Local, Definition)
+	(Local, Definition)
       | IDENT "Example" ->
-	no_hook, (Global, Example)
+	(Global, Example)
       | IDENT "SubClass"  ->
-          Class.add_subclass_hook, (use_locality_exp (), SubClass) ] ]
+        (use_locality_exp (), SubClass) ] ]
   ;
   assumption_token:
     [ [ "Hypothesis" -> (Local, Logical)
@@ -534,16 +533,15 @@ GEXTEND Gram
           d = def_body ->
           let s = coerce_reference_to_id qid in
 	  VernacDefinition
-	    ((Global,CanonicalStructure),(Loc.ghost,s),d,
-	     (fun _ -> Recordops.declare_canonical_structure))
+	    ((Global,CanonicalStructure),(Loc.ghost,s),d)
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((use_locality_exp (),Coercion),(Loc.ghost,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((use_locality_exp (),Coercion),(Loc.ghost,s),d)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_reference_to_id qid in
-	  VernacDefinition ((enforce_locality_exp true,Coercion),(Loc.ghost,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((enforce_locality_exp true,Coercion),(Loc.ghost,s),d)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
 	   VernacIdentityCoercion (enforce_locality_exp true, f, s, t)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c04b99c5d9..14ca732a4e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -585,7 +585,7 @@ let rec pr_vernac = function
       pr_syntax_modifiers l
 
   (* Gallina *)
-  | VernacDefinition (d,id,b,f) -> (* A verifier... *)
+  | VernacDefinition (d,id,b) -> (* A verifier... *)
       let pr_def_token dk = str (Kindops.string_of_definition_kind dk) in
       let pr_reduce = function
         | None -> mt()
@@ -608,7 +608,7 @@ let rec pr_vernac = function
         | None -> mt()
         | Some cc -> str" :=" ++ spc() ++ cc))
 
-  | VernacStartTheoremProof (ki,l,_,_) ->
+  | VernacStartTheoremProof (ki,l,_) ->
       hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
              prlist (pr_statement (spc () ++ str "with")) (List.tl l))
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8fb3aa66b6..a4052ac821 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -449,14 +449,22 @@ let start_proof_and_print k l hook =
   start_proof_com k l hook;
   print_subgoals ()
 
-let vernac_definition (local,k) (loc,id as lid) def hook =
+let no_hook _ _ = ()
+
+let vernac_definition_hook = function
+| Coercion -> Class.add_coercion_hook
+| CanonicalStructure -> fun _ -> Recordops.declare_canonical_structure
+| SubClass -> Class.add_subclass_hook
+| _ -> no_hook
+
+let vernac_definition (local,k) (loc,id as lid) def =
+  let hook = vernac_definition_hook k in
   if local == Local then Dumpglob.dump_definition lid true "var"
   else Dumpglob.dump_definition lid false "def";
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
- 	let hook _ _ = () in
  	  start_proof_and_print (local,DefinitionBody Definition)
-	    [Some lid, (bl,t,None)] hook
+	    [Some lid, (bl,t,None)] no_hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
@@ -465,7 +473,7 @@ let vernac_definition (local,k) (loc,id as lid) def hook =
  		Some (snd (interp_redexp env evc r)) in
 	do_definition id (local,k) bl red_option c typ_opt hook)
 
-let vernac_start_proof kind l lettop hook =
+let vernac_start_proof kind l lettop =
   if Dumpglob.dump () then
     List.iter (fun (id, _) ->
       match id with
@@ -475,7 +483,7 @@ let vernac_start_proof kind l lettop hook =
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode.");
-  start_proof_and_print (Global, Proof kind) l hook
+  start_proof_and_print (Global, Proof kind) l no_hook
 
 let qed_display_script = ref true
 
@@ -1668,8 +1676,8 @@ let interp c = match c with
   | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
 
   (* Gallina *)
-  | VernacDefinition (k,lid,d,f) -> vernac_definition k lid d f
-  | VernacStartTheoremProof (k,l,top,f) -> vernac_start_proof k l top f
+  | VernacDefinition (k,lid,d) -> vernac_definition k lid d
+  | VernacStartTheoremProof (k,l,top) -> vernac_start_proof k l top
   | VernacEndProof e -> vernac_end_proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
@@ -1755,7 +1763,7 @@ let interp c = match c with
   | VernacNop -> ()
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false (fun _ _->())
+  | VernacGoal t -> vernac_start_proof Theorem [None,([],t,None)] false
   | VernacAbort id -> vernac_abort id
   | VernacAbortAll -> vernac_abort_all ()
   | VernacRestart -> vernac_restart ()