From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 tools/coqdoc/index.ml | 44 +++++---------------------------------------
 1 file changed, 5 insertions(+), 39 deletions(-)

(limited to 'tools/coqdoc/index.ml')

diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 8170e173..4a5ff592 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Filename
-open Lexing
 open Printf
 open Cdglobals
 
@@ -36,7 +34,6 @@ type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
 
-let current_type : entry_type ref = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
@@ -95,9 +92,6 @@ let empty_stack = []
 let module_stack = ref empty_stack
 let section_stack = ref empty_stack
 
-let init_stack () =
-  module_stack := empty_stack; section_stack := empty_stack
-
 let push st p = st := p::!st
 let pop st =
   match !st with
@@ -109,27 +103,6 @@ let head st =
     | [] -> ""
     | x::_ -> x
 
-let begin_module m = push module_stack m
-let begin_section s = push section_stack s
-
-let end_block id =
-  (** determines if it ends a module or a section and pops the stack *)
-  if ((String.compare (head !module_stack) id ) == 0) then
-    pop module_stack
-  else if ((String.compare (head !section_stack) id) == 0) then
-    pop section_stack
-  else
-    ()
-
-let make_fullid id =
-  (** prepends the current module path to an id *)
-  let path = string_of_stack !module_stack in
-    if String.length path > 0 then
-      path ^ "." ^ id
-    else
-      id
-
-
 (* Coq modules *)
 
 let split_sp s =
@@ -158,7 +131,7 @@ let find_external_library logicalpath =
   let rec aux = function
     | [] -> raise Not_found
     | (l,u)::rest ->
-        if String.length logicalpath > String.length l &
+        if String.length logicalpath > String.length l &&
           String.sub logicalpath 0 (String.length l + 1) = l ^"."
         then u
         else aux rest
@@ -208,10 +181,6 @@ let sort_entries el =
 
 let display_letter c = if c = '*' then "other" else String.make 1 c
 
-let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
-
-let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
-
 let type_name = function
   | Library ->
       let ln = !lib_name in
@@ -304,9 +273,9 @@ let type_of_string = function
   | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
   | "ex" | "scheme" -> Definition
   | "prf" | "thm" -> Lemma
-  | "ind" | "coind" -> Inductive
+  | "ind" | "variant" | "coind" -> Inductive
   | "constr" -> Constructor
-  | "rec" | "corec" -> Record
+  | "indrec" | "rec" | "corec" -> Record
   | "proj" -> Projection
   | "class" -> Class
   | "meth" -> Method
@@ -319,7 +288,7 @@ let type_of_string = function
   | "mod" | "modtype" -> Module
   | "tac" -> TacticDefinition
   | "sec" -> Section
-  | s -> raise (Invalid_argument ("type_of_string:" ^ s))
+  | s -> invalid_arg ("type_of_string:" ^ s)
 
 let ill_formed_glob_file f =
   eprintf "Warning: ill-formed file %s (links will not be available)\n" f
@@ -370,9 +339,6 @@ let read_glob vfile f =
 		    done)
 	       with _ -> ())
 	  | _ ->
-	      try Scanf.sscanf s "not %d %s %s"
-		(fun loc sp id -> add_def loc loc (type_of_string "not") sp id)
-	      with Scanf.Scan_failure _ ->
 	      try Scanf.sscanf s "%s %d:%d %s %s"
 		(fun ty loc1 loc2 sp id ->
                   add_def loc1 loc2 (type_of_string ty) sp id)
-- 
cgit v1.2.3