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

6 files changed, 20 insertions, 19 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index acf1ae838..d10c8f68c 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 -> 
diff --git a/ide/coq.ml b/ide/coq.ml
index c4b6c34b2..2c8d7b8db 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -273,6 +273,7 @@ let rec attribute_of_vernac_command = function
 
   (* Commands *)
   | VernacDeclareTacticDefinition _ -> []
+  | VernacCreateHintDb _ -> []
   | VernacHints _ -> []
   | VernacSyntacticDefinition _ -> []
   | VernacDeclareImplicits _ -> []
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 3f315ccb7..d12c21b15 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -58,11 +58,13 @@ Inductive term : ctx -> type -> Type :=
 
 Hint Constructors term : lambda.
 
+Open Local Scope context_scope.
+
 Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope.
 
 Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> 
   forall τ', term (Γ ,, τ' ;; Δ) τ.
-Proof with simpl in * ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda.
+Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda.
   intros Γ Δ τ H.
 
   dependent induction H.
@@ -81,7 +83,7 @@ Proof with simpl in * ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda
 Qed.
 
 Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ.
-Proof with simpl in * ; simplify_dep_elim ; simplify_IH_hyps ; auto.
+Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto.
   intros until 1.
   dependent induction H.
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 5b5425590..b41c19ac3 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -66,18 +66,20 @@ let full_ident sp id =
     
 let add_def loc ty sp id = 
   Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
-  Hashtbl.add deftable (!current_library, id) (Def (full_ident sp id, ty))
+  Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
     
 let add_ref m loc m' sp id ty = 
-  Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty))
+  if Hashtbl.mem reftable (m, loc) then ()
+  else
+    Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty))
     
 let add_mod m loc m' id = 
   Hashtbl.add reftable (m, loc) (Mod (m', id));
-  Hashtbl.add deftable (m, id) (Mod (m', id))
+  Hashtbl.add deftable id (Mod (m', id))
     
 let find m l = Hashtbl.find reftable (m, l)
   
-let find_string m s = Hashtbl.find deftable (m, s)
+let find_string m s = Hashtbl.find deftable s
   
 (*s Manipulating path prefixes *) 
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index a7ed7444a..2d547af79 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -273,8 +273,8 @@ module Latex = struct
 	  end else begin
 	    if !Cdglobals.interpolate then
 	      try reference s (Index.find_string !current_module s)
-	      with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" 
-	    else printf "\\coqdocvar{"; raw_ident s; printf "}"
+	      with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}"
+	    else (printf "\\coqdocvar{"; raw_ident s; printf "}")
 	  end
       end
     end
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d4c396d49..8c0e7e05a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -375,7 +375,7 @@ let vernac_assumption kind l nl=
 let vernac_inductive f indl = 
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, cstrs), _) ->
-      Dumpglob.dump_definition lid false"ind";
+      Dumpglob.dump_definition lid false "ind";
       List.iter (fun (_, (lid, _)) ->
 	Dumpglob.dump_definition lid false "constr") cstrs)
       indl;