Suite commit 11236

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

8 files changed, 117 insertions, 81 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index fbb4589b8..c36c6458d 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -140,7 +140,7 @@ let subtac (loc, command) =
   match command with
   | VernacDefinition (defkind, (_, id as lid), expr, hook) -> 
       check_fresh lid;
-      if Dumpglob.dump () then dump_definition lid "def";
+      dump_definition lid "def";
       (match expr with
       | ProveBody (bl, t) -> 
 	  if Lib.is_modtype () then
@@ -153,12 +153,12 @@ let subtac (loc, command) =
   | VernacFixpoint (l, b) -> 
       List.iter (fun ((lid, _, _, _, _), _) -> 
 	check_fresh lid;
-	if Dumpglob.dump () then dump_definition lid "fix") l;
+	dump_definition lid "fix") l;
       let _ = trace (str "Building fixpoint") in
 	ignore(Subtac_command.build_recursive l b)
 	  
   | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
-      if Dumpglob.dump () then dump_definition id "prf";
+      dump_definition id "prf";
       if not(Pfedit.refining ()) then
 	if lettop then
 	  errorlabstrm "Subtac_command.StartProof"
@@ -173,7 +173,7 @@ let subtac (loc, command) =
       vernac_assumption env isevars stre l nl
 	
   | VernacInstance (glob, sup, is, props, pri) ->
-      if Dumpglob.dump () then dump_constraint "inst" is;
+      dump_constraint "inst" is;
       ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 	
   | VernacCoFixpoint (l, b) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fccfb1bf3..26ed02379 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -252,7 +252,7 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
 let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
   let ntn,args = contract_notation ntn args in
   let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-    if Dumpglob.dump () then Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
+    Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
     let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
       subst_aconstr_in_rawconstr loc intern subst ([],env) c
 
@@ -334,10 +334,10 @@ let check_no_explicitation l =
 let intern_qualid loc qid intern env args =
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
-      if Dumpglob.dump() then Dumpglob.add_glob loc ref;
+      Dumpglob.add_glob loc ref;
       RRef (loc, ref), args
   | SyntacticDef sp ->
-      if Dumpglob.dump() then Dumpglob.add_glob_kn loc sp;
+      Dumpglob.add_glob_kn loc sp;
       let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
       let nids = List.length ids in
       if List.length args < nids then error_not_enough_arguments loc;
@@ -567,7 +567,7 @@ let find_constructor ref f aliases pats scopes =
 	    let v = Environ.constant_value (Global.env()) cst in
 	    unf (global_of_constr v)
         | ConstructRef cstr -> 
-	    if Dumpglob.dump() then Dumpglob.add_glob loc r; 
+	    Dumpglob.add_glob loc r; 
 	    cstr, [], pats
         | _ -> raise Not_found
       in unf r
@@ -618,7 +618,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
       let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-      if Dumpglob.dump () then Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
+      Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
       let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes 
 	c
@@ -627,7 +627,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
       let a = alias_of aliases in
       let (c,df) = Notation.interp_prim_token_cases_pattern loc p a 
 	(tmp_scope,scopes) in
-      if Dumpglob.dump () then Dumpglob.dump_notation_location (fst (unloc loc)) df;
+      Dumpglob.dump_notation_location (fst (unloc loc)) df;
       (ids,[subst,c])
   | CPatDelimiters (loc, key, e) ->
       intern_pat (find_delimiters_scope loc key::scopes) aliases None e
@@ -687,7 +687,7 @@ let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
   | Anonymous -> env 
   | Name id -> 
       check_hidden_implicit_parameters id lvar;
-      if Dumpglob.dump() then Dumpglob.dump_binding loc id;
+      Dumpglob.dump_binding loc id;
       (Idset.add id ids,tmpsc,scopes)
 
 let intern_typeclass_binders intern_type lvar env bl =
@@ -887,7 +887,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
         intern_notation intern env loc ntn args
     | CPrim (loc, p) ->
 	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
-	if Dumpglob.dump () then Dumpglob.dump_notation_location (fst (unloc loc)) df;
+	Dumpglob.dump_notation_location (fst (unloc loc)) df;
 	c
     | CDelimiters (loc, key, e) ->
 	intern (ids,None,find_delimiters_scope loc key::scopes) e
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index a8f4b31d2..0035b3f07 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -9,8 +9,6 @@
 (* $Id$ *)
 
 
-let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl
-
 (* Dump of globalization (to be used by coqdoc) *)
 
 let glob_file = ref Pervasives.stdout
@@ -130,16 +128,17 @@ let dump_ref loc filepath modpath ident ty =
 		  (fst (Util.unloc loc)) filepath modpath ident ty)
 
 let add_glob_gen loc sp lib_dp ty =
-  let mod_dp,id = Libnames.repr_path sp in
-  let mod_dp = remove_sections mod_dp in
-  let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
-  let filepath = Names.string_of_dirpath lib_dp in
-  let modpath = Names.string_of_dirpath mod_dp_trunc in
-  let ident = Names.string_of_id id in
-    dump_ref loc filepath modpath ident ty
+  if dump () then
+    let mod_dp,id = Libnames.repr_path sp in
+    let mod_dp = remove_sections mod_dp in
+    let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
+    let filepath = Names.string_of_dirpath lib_dp in
+    let modpath = Names.string_of_dirpath mod_dp_trunc in
+    let ident = Names.string_of_id id in
+      dump_ref loc filepath modpath ident ty
 
 let add_glob loc ref = 
-  if loc <> Util.dummy_loc then
+  if dump () && loc <> Util.dummy_loc then
     let sp = Nametab.sp_of_global ref in
     let lib_dp = Lib.library_part ref in
     let ty = type_of_global_ref ref in
@@ -150,7 +149,7 @@ let mp_of_kn kn =
     Names.MPdot (mp,l) 
 
 let add_glob_kn loc kn =
-  if loc <> Util.dummy_loc then
+  if dump () && loc <> Util.dummy_loc then
     let sp = Nametab.sp_of_syntactic_definition kn in
     let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
       add_glob_gen loc sp lib_dp "syndef"
@@ -167,21 +166,6 @@ let add_local loc id = ()
 
 let dump_binding loc id = ()
       
-(* BEGIN obsolete *)
-
-let dump_modref qid = Pp.warning ("Dumpglob.modref: not yet implemented")
-  
-let dump_def loc ref = 
-  let curr_mp, _ = Lib.current_prefix() in
-  let lib_dp, curr_dp = Lib.split_mp curr_mp in
-  let mod_dp_trunc =  Libnames.drop_dirpath_prefix lib_dp curr_dp in
-
-  let fullname = Libnames.string_of_qualid (Libnames.make_qualid mod_dp_trunc ref) in
-  let filepath = Names.string_of_dirpath lib_dp in
-    dump_string (Printf.sprintf "D%d %s %s\n" (fst (Util.unloc loc)) filepath fullname)
-
-(* END obsolete *)
-
 let dump_definition (loc, id) sec s =
   dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc)) 
 			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
@@ -197,43 +181,47 @@ let dump_constraint ((loc, n), _, _) sec ty =
 
 let dump_name (loc, n) sec ty =
   match n with
-  | Names.Name id -> dump_definition (loc, id) sec ty
-  | Names.Anonymous -> ()
+    | Names.Name id -> dump_definition (loc, id) sec ty
+    | Names.Anonymous -> ()
 
 let dump_local_binder b sec ty =
-  match b with
-  | Topconstr.LocalRawAssum (nl, _, _) -> 
-      List.iter (fun x -> dump_name x sec ty) nl
-  | Topconstr.LocalRawDef _ -> ()
+  if dump () then
+    match b with
+      | Topconstr.LocalRawAssum (nl, _, _) -> 
+	  List.iter (fun x -> dump_name x sec ty) nl
+      | Topconstr.LocalRawDef _ -> ()
 
 let dump_modref loc mp ty =
-  let (dp, l) = Lib.split_modpath mp in
-  let fp = Names.string_of_dirpath dp in
-  let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in
-    dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
-		    (fst (Util.unloc loc)) fp mp "<>" ty)
+  if dump () then
+    let (dp, l) = Lib.split_modpath mp in
+    let fp = Names.string_of_dirpath dp in
+    let mp = Names.string_of_dirpath (Names.make_dirpath (Util.list_drop_last l)) in
+      dump_string (Printf.sprintf "R%d %s %s %s %s\n" 
+		      (fst (Util.unloc loc)) fp mp "<>" ty)
 
 let dump_moddef loc mp ty =
-  let (dp, l) = Lib.split_modpath mp in
-  let mp = Names.string_of_dirpath (Names.make_dirpath l) in
-    dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
+  if dump () then
+    let (dp, l) = Lib.split_modpath mp in
+    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
 
 let dump_libref loc dp ty =
   dump_string (Printf.sprintf "R%d %s <> <> %s\n" 
 		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
 let dump_notation_location pos ((path,df),sc) =
-  let rec next growing =
-    let loc = Lexer.location_function !token_number in
-    let (bp,_) = Util.unloc loc in
-      if growing then if bp >= pos then loc else (incr token_number; next true)
-      else if bp = pos then loc
-      else if bp > pos then (decr token_number;next false)
-      else (incr token_number;next true) in
-  let loc = next (pos >= !last_pos) in
-    last_pos := pos;
-    let path = Names.string_of_dirpath path in
-    let _sc = match sc with Some sc -> " "^sc | _ -> "" in
-      dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
+  if dump () then
+    let rec next growing =
+      let loc = Lexer.location_function !token_number in
+      let (bp,_) = Util.unloc loc in
+	if growing then if bp >= pos then loc else (incr token_number; next true)
+	else if bp = pos then loc
+	else if bp > pos then (decr token_number;next false)
+	else (incr token_number;next true) in
+    let loc = next (pos >= !last_pos) in
+      last_pos := pos;
+      let path = Names.string_of_dirpath path in
+      let _sc = match sc with Some sc -> " "^sc | _ -> "" in
+	dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
 
 
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
new file mode 100644
index 000000000..2f36c25c5
--- /dev/null
+++ b/interp/dumpglob.mli
@@ -0,0 +1,43 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+
+val open_glob_file : string -> unit
+val close_glob_file : unit -> unit
+
+val dump : unit -> bool
+val multi_dump : unit -> bool
+
+val noglob : unit -> unit
+val dump_to_stdout : unit -> unit
+val dump_into_file : string -> unit
+val dump_to_dotglob : unit -> unit
+
+val pause : unit -> unit
+val continue : unit -> unit
+
+val coqdoc_freeze : unit -> Lexer.location_table * int * int
+val coqdoc_unfreeze : Lexer.location_table * int * int -> unit
+
+val add_glob : Util.loc -> Libnames.global_reference -> unit
+val add_glob_kn : Util.loc -> Names.kernel_name -> unit
+
+val dump_definition : Util.loc * Names.identifier -> bool -> string -> unit
+val dump_moddef : Util.loc -> Names.module_path -> string -> unit
+val dump_modref  : Util.loc -> Names.module_path -> string -> unit
+val dump_reference  : Util.loc -> string -> string -> string -> unit
+val dump_libref : Util.loc -> Names.dir_path -> string -> unit
+val dump_notation_location : int -> (Notation.notation_location * Topconstr.scope_name option) -> unit
+val dump_binding : Util.loc -> Names.Idset.elt -> unit
+val dump_constraint :  Topconstr.typeclass_constraint -> bool -> string -> unit
+val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit
+
+val dump_string : string -> unit
+
diff --git a/lib/util.ml b/lib/util.ml
index 2a60ad7b0..549b79e78 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -863,6 +863,10 @@ let list_cartesians op init ll =
 
 let list_combinations l = list_cartesians (fun x l -> x::l) [] l
 
+(* Drop the last element of a list *)
+
+let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index a341fa5a2..d845dd2eb 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -156,6 +156,7 @@ val list_skipn : int -> 'a list -> 'a list
 val list_addn : int -> 'a -> 'a list -> 'a list
 val list_prefix_of : 'a list -> 'a list -> bool
 val list_drop_prefix : 'a list -> 'a list -> 'a list
+val list_drop_last : 'a list -> 'a list
 (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
 val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6641289eb..c7e2230fd 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -478,7 +478,7 @@ let add_hints local dbnames0 h =
             (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
              str "to an evaluable reference.")
         in
-	  if Dumpglob.dump () then Dumpglob.add_glob (loc_of_reference r) gr;
+	  Dumpglob.add_glob (loc_of_reference r) gr;
 	 (gr,r') in
       add_unfolds (List.map f lhints) local dbnames
   | HintsConstructors lqid ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index afa667ad9..a674bc3b7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -277,7 +277,7 @@ let print_located_module r =
 
 let global_with_alias r =
   let gr = global_with_alias r in
-    if Dumpglob.dump () then Dumpglob.add_glob (loc_of_reference r) gr;
+    Dumpglob.add_glob (loc_of_reference r) gr;
     gr
 
 (**********)
@@ -308,7 +308,7 @@ let start_proof_and_print k l hook =
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
 let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
-  if Dumpglob.dump () then Dumpglob.dump_definition lid false "def";
+  Dumpglob.dump_definition lid false "def";
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
  	if Lib.is_modtype () then
@@ -421,7 +421,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
     Modintern.interp_modtype Modintern.interp_modexpr
     id binders_ast (Some mty_ast_o) None
   in 
-    if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod";
+    Dumpglob.dump_moddef loc mp "mod";
     if_verbose message ("Module "^ string_of_id id ^" is declared");
     Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
@@ -441,7 +441,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
        let mp = Declaremods.start_module Modintern.interp_modtype export
 	 id binders_ast mty_ast_o 
        in
-	 if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod";
+	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message 
 	   ("Interactive Module "^ string_of_id id ^" started") ;
          List.iter
@@ -461,7 +461,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
 	  Modintern.interp_modtype Modintern.interp_modexpr
 	  id binders_ast mty_ast_o mexpr_ast_o 
        in
-	 if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod";
+	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose message 
 	   ("Module "^ string_of_id id ^" is defined");
          Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
@@ -469,7 +469,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
 
 let vernac_end_module export (loc,id) =
   let mp = Declaremods.end_module id in
-    if Dumpglob.dump () then Dumpglob.dump_modref loc mp "mod";
+    Dumpglob.dump_modref loc mp "mod";
     if_verbose message ("Module "^ string_of_id id ^" is defined") ;
     Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
@@ -487,7 +487,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
            (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
              ([],[]) in
        let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
-        if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "modtype";
+        Dumpglob.dump_moddef loc mp "modtype";
 	if_verbose message 
 	  ("Interactive Module Type "^ string_of_id id ^" started");
         List.iter
@@ -506,14 +506,14 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
             else (idl,ty)) binders_ast in
 	let mp = Declaremods.declare_modtype Modintern.interp_modtype 
 	  id binders_ast base_mty in
-          if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "modtype";
+          Dumpglob.dump_moddef loc mp "modtype";
 	  if_verbose message 
 	    ("Module Type "^ string_of_id id ^" is defined")
 
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype id in
-    if Dumpglob.dump () then Dumpglob.dump_modref loc mp "modtype";
+    Dumpglob.dump_modref loc mp "modtype";
     if_verbose message 
       ("Module Type "^ string_of_id id ^" is defined")
 
@@ -532,7 +532,7 @@ let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd (snd struc))
     | Some (_,id as lid) ->
-	if Dumpglob.dump () then Dumpglob.dump_definition lid false "constr"; id in
+	Dumpglob.dump_definition lid false "constr"; id in
   let sigma = Evd.empty in
   let env = Global.env() in
   let s = interp_constr sigma env sort in
@@ -553,11 +553,11 @@ let vernac_record struc binders sort nameopt cfs =
 
 let vernac_begin_section (_, id as lid) =
   check_no_pending_proofs ();
-  if Dumpglob.dump () then Dumpglob.dump_definition lid true "sec";
+  Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
 let vernac_end_section (loc, id) = 
-  if Dumpglob.dump () then 
+  
     Dumpglob.dump_reference loc 
       (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
   Lib.close_section id
@@ -603,15 +603,15 @@ let vernac_class id par ar sup props =
   Classes.new_class id par ar sup props
  
 let vernac_instance glob sup inst props pri =
-  if Dumpglob.dump () then Dumpglob.dump_constraint inst false "inst";
+  Dumpglob.dump_constraint inst false "inst";
   ignore(Classes.new_instance ~global:glob sup inst props pri)
 
 let vernac_context l =
-  if Dumpglob.dump () then List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
+  List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
   Classes.context l
 
 let vernac_declare_instance id =
-  if Dumpglob.dump () then Dumpglob.dump_definition id false "inst";
+  Dumpglob.dump_definition id false "inst";
   Classes.declare_instance false id
 
 (***********)
@@ -746,7 +746,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition lid =
-  if Dumpglob.dump () then Dumpglob.dump_definition lid false "syndef";
+  Dumpglob.dump_definition lid false "syndef";
   Command.syntax_definition (snd lid)
   
 let vernac_declare_implicits local r = function