Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition

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

2 files changed, 13 insertions, 11 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a0137d7911..82318340cc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -252,7 +252,7 @@ let start_proof_and_print idopt k t hook =
   print_subgoals ();
   if !pcoq <> None then (out_some !pcoq).start_proof ()
 
-let vernac_definition local id def hook =
+let vernac_definition (local,_ as k) id def hook =
   match def with
   | ProveBody (bl,t) ->   (* local binders, typ *)
       if Lib.is_modtype () then
@@ -268,7 +268,7 @@ let vernac_definition local id def hook =
         | Some r -> 
 	    let (evc,env)= Command.get_current_context () in
 	    Some (interp_redexp env evc r) in
-      declare_definition id local bl red_option c typ_opt hook
+      declare_definition id k bl red_option c typ_opt hook
 
 let vernac_start_proof kind sopt (bl,t) lettop hook =
   if not(refining ()) then
@@ -883,8 +883,8 @@ let interp_search_restriction = function
 open Search
 
 let interp_search_about_item = function
-  | SearchRef qid -> SearchRef (Nametab.global qid)
-  | SearchString s as x -> x
+  | SearchRef qid -> GlobSearchRef (Nametab.global qid)
+  | SearchString s -> GlobSearchString s
 
 let vernac_search s r =
   let r = interp_search_restriction r in
@@ -1119,7 +1119,7 @@ let interp c = match c with
       vernac_notation local c infpl mv8 sc
 
   (* Gallina *)
-  | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f
+  | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
   | VernacStartTheoremProof (k,id,t,top,f) ->
       vernac_start_proof k (Some id) t top f
   | VernacEndProof e -> vernac_end_proof e
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 76c3358a02..06dae38155 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -55,11 +55,15 @@ type printable =
   | PrintScope of string
   | PrintAbout of reference
 
+type search_about_item =
+  | SearchRef of reference
+  | SearchString of string
+
 type searchable =
   | SearchPattern of pattern_expr
   | SearchRewrite of pattern_expr
   | SearchHead of reference
-  | SearchAbout of reference Search.search_about_item list
+  | SearchAbout of search_about_item list
   | SearchNamed of string list
 
 type locatable =
@@ -92,14 +96,12 @@ type comment =
   | CommentString of string
   | CommentInt of int
 
-type raw_constr_expr = constr_expr
-
 type hints =
   | HintsResolve of (identifier option * constr_expr) list
   | HintsImmediate of (identifier option * constr_expr) list
   | HintsUnfold of (identifier option * reference) list
   | HintsConstructors of identifier option * reference list
-  | HintsExtern of identifier option * int * raw_constr_expr * raw_tactic_expr
+  | HintsExtern of identifier option * int * constr_expr * raw_tactic_expr
   | HintsDestruct of identifier *
       int * (bool,unit) location * constr_expr * raw_tactic_expr
 
@@ -178,8 +180,8 @@ type vernac_expr =
       (string * syntax_modifier list) option * scope_name option
 
   (* Gallina *)
-  | VernacDefinition of definition_kind * identifier * definition_expr *
-      declaration_hook * definitionkind
+  | VernacDefinition of definition_kind * identifier * definition_expr * 
+      declaration_hook
   | VernacStartTheoremProof of theorem_kind * identifier *
       (local_binder list * constr_expr) * bool * declaration_hook
   | VernacEndProof of proof_end