Minor fixes related to coqdoc and --interpolate and the dependent

induction test-suite script.


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

1 files changed, 6 insertions, 10 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index acf1ae8386..d10c8f68c2 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -104,13 +104,9 @@ let declare_assumption env isevars idl is_coe k bl c nl =
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
 
-let dump_definition (loc, id) s =
-  Dumpglob.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) 
-			   (string_of_id id))
-
 let dump_constraint ty ((loc, n), _, _) =
   match n with
-    | Name id -> dump_definition (loc, id) ty
+    | Name id -> Dumpglob.dump_definition (loc, id) false ty
     | Anonymous -> ()
 
 let dump_variable lid = ()
@@ -120,7 +116,7 @@ let vernac_assumption env isevars kind l nl =
     List.iter (fun (is_coe,(idl,c)) -> 
       if Dumpglob.dump () then
 	List.iter (fun lid -> 
-	  if global then dump_definition lid "ax" 
+	  if global then Dumpglob.dump_definition lid (not global) "ax"
 	  else dump_variable lid) idl;
       declare_assumption env isevars idl is_coe kind [] c nl) l
 
@@ -138,7 +134,7 @@ let subtac (loc, command) =
   match command with
   | VernacDefinition (defkind, (_, id as lid), expr, hook) -> 
       check_fresh lid;
-      dump_definition lid "def";
+      Dumpglob.dump_definition lid false "def";
       (match expr with
       | ProveBody (bl, t) -> 
 	  if Lib.is_modtype () then
@@ -151,12 +147,12 @@ let subtac (loc, command) =
   | VernacFixpoint (l, b) -> 
       List.iter (fun ((lid, _, _, _, _), _) -> 
 	check_fresh lid;
-	dump_definition lid "fix") l;
+	Dumpglob.dump_definition lid false "fix") l;
       let _ = trace (str "Building fixpoint") in
 	ignore(Subtac_command.build_recursive l b)
 	  
   | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
-      dump_definition id "prf";
+      Dumpglob.dump_definition id false "prf";
       if not(Pfedit.refining ()) then
 	if lettop then
 	  errorlabstrm "Subtac_command.StartProof"
@@ -176,7 +172,7 @@ let subtac (loc, command) =
 	
   | VernacCoFixpoint (l, b) ->
       if Dumpglob.dump () then 
-	List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l;
+	List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
       ignore(Subtac_command.build_corecursive l b)
 	
   (*| VernacEndProof e ->