Remove some more "open" and dead code thanks to OCaml4 warnings

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

5 files changed, 2 insertions, 107 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a2be41700e..c204db0e01 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -110,13 +110,11 @@ let global_reference_in_absolute_module dir id =
 
 type internalization_error =
   | VariableCapture of identifier * identifier
-  | WrongExplicitImplicit
   | IllegalMetavariable
   | NotAConstructor of reference
   | UnboundFixName of bool * identifier
   | NonLinearPattern of identifier
   | BadPatternsNumber of int * int
-  | BadExplicitationNumber of explicitation * int option
 
 exception InternalizationError of Loc.t * internalization_error
 
@@ -124,10 +122,6 @@ let explain_variable_capture id id' =
   pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++
   strbrk ": cannot interpret both of them with the same type"
 
-let explain_wrong_explicit_implicit =
-  str "Found an explicitly given implicit argument but was expecting" ++
-  fnl () ++ str "a regular one"
-
 let explain_illegal_metavariable =
   str "Metavariables allowed only in patterns"
 
@@ -146,32 +140,15 @@ let explain_bad_patterns_number n1 n2 =
   str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++
   str " but found " ++ int n2
 
-let explain_bad_explicitation_number n po =
-  match n with
-  | ExplByPos (n,_id) ->
-      let s = match po with
-	| None -> str "a regular argument"
-	| Some p -> int p in
-      str "Bad explicitation number: found " ++ int n ++
-      str" but was expecting " ++ s
-  | ExplByName id ->
-      let s = match po with
-	| None -> str "a regular argument"
-	| Some p -> (*pr_id (name_of_position p) in*) failwith "" in
-      str "Bad explicitation name: found " ++ pr_id id ++
-      str" but was expecting " ++ s
-
 let explain_internalization_error e =
   let pp = match e with
   | VariableCapture (id,id') -> explain_variable_capture id id'
-  | WrongExplicitImplicit -> explain_wrong_explicit_implicit
   | IllegalMetavariable -> explain_illegal_metavariable
   | NotAConstructor ref -> explain_not_a_constructor ref
   | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
   | NonLinearPattern id -> explain_non_linear_pattern id
   | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
-  | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in
-  pp ++ str "."
+  in pp ++ str "."
 
 let error_bad_inductive_type loc =
   user_err_loc (loc,"",str
@@ -283,10 +260,6 @@ let error_inconsistent_scope loc id scopes1 scopes2 =
     pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++
     pr_scope_stack scopes1)
 
-let error_expect_constr_notation_type loc id =
-  user_err_loc (loc,"",
-    pr_id id ++ str " is bound in the notation to a term variable.")
-
 let error_expect_binder_notation_type loc id =
   user_err_loc (loc,"",
     pr_id id ++
@@ -786,12 +759,6 @@ let product_of_cases_patterns ids idspl =
 	 List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)))
     idspl (ids,[[],[]])
 
-let simple_product_of_cases_patterns pl =
-  List.fold_right (fun pl ptaill ->
-    List.flatten (List.map (fun (subst,p) ->
-      List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl))
-    pl [[],[]]
-
 (* @return the first variable that occurs twice in a pattern
 
 naive n2 algo *)
@@ -1769,8 +1736,6 @@ open Environ
 let my_intern_constr sigma env lvar acc c =
   internalize sigma env acc false lvar c
 
-let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
-
 let intern_context global_level sigma env impl_env params =
   try
   let lvar = (([],[]), []) in
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 0f386ec04b..f91d9ff221 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,9 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
-open Names
 open Entries
 open Libnames
 open Constrexpr
@@ -28,8 +25,6 @@ val error_not_a_functor :  module_struct_entry -> 'a
 
 val error_not_equal : module_path -> module_path -> 'a
 
-val error_result_must_be_signature : unit -> 'a
-
 oval error_not_a_modtype_loc : loc -> string -> 'a
 
 val error_not_a_module_loc : loc -> string -> 'a
@@ -41,9 +36,6 @@ val error_with_in_module : unit -> 'a
 val error_application_to_module_type : unit -> 'a
 *)
 
-let error_result_must_be_signature () =
-  error "The result module type must be a signature."
-
 let error_not_a_modtype_loc loc s =
   Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s))
 
@@ -60,53 +52,6 @@ let error_application_to_module_type loc =
   Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
 
 
-
-
-let rec make_mp mp = function
-    [] -> mp
-  | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
-
-(*
-(* Since module components are not put in the nametab we try to locate
-the module prefix *)
-exception BadRef
-
-let lookup_qualid (modtype:bool) qid =
-  let rec make_mp mp = function
-      [] -> mp
-    | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
-  in
-  let rec find_module_prefix dir n =
-    if n<0 then raise Not_found;
-    let dir',dir'' = List.chop n dir in
-    let id',dir''' =
-      match dir'' with
-	| hd::tl -> hd,tl
-	| _ -> anomaly "This list should not be empty!"
-    in
-    let qid' = make_qualid dir' id' in
-      try
-	match Nametab.locate qid' with
-	  | ModRef mp -> mp,dir'''
-	  | _ -> raise BadRef
-      with
-	  Not_found -> find_module_prefix dir (pred n)
-  in
-    try Nametab.locate qid
-    with Not_found ->
-      let (dir,id) = repr_qualid qid in
-      let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
-      let mp =
-	List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
-      in
-	if modtype then
-	  ModTypeRef (make_ln mp (label_of_id id))
-	else
-	  ModRef (MPdot (mp,label_of_id id))
-
-*)
-
-
 (* Search for the head of [qid] in [binders].
    If found, returns the module_path/kernel_name created from the dirpath
    and the basename. Searches Nametab otherwise.
diff --git a/interp/notation.ml b/interp/notation.ml
index 46a06b7001..d7f539f2f7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -399,8 +399,6 @@ let interp_notation loc ntn local_scopes =
     user_err_loc
     (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
 
-let isGApp = function GApp _ -> true | _ -> false
-
 let uninterp_notations c =
   List.map_append (fun key -> Gmapl.find key !notations_key_table)
     (glob_constr_keys c)
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index b38177d48b..adf611b563 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -14,7 +14,6 @@
 (* *)
 open Pp
 open Errors
-open Util
 open Libnames
 open Globnames
 open Misctypes
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index abdde1f549..dd656d479c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -20,7 +20,7 @@ open Constrexpr_ops
 
 
 let oldfashion_patterns = ref (true)
-let write_oldfashion_patterns = Goptions.declare_bool_option {
+let _ = Goptions.declare_bool_option {
   Goptions.optsync = true; Goptions.optdepr = false;
   Goptions.optname =
     "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
@@ -244,18 +244,6 @@ let rec replace_vars_constr_expr l = function
   | c -> map_constr_expr_with_binders List.remove_assoc
            replace_vars_constr_expr l c
 
-(**********************************************************************)
-(* Concrete syntax for modules and modules types *)
-
-type with_declaration_ast =
-  | CWith_Module of identifier list Loc.located * qualid Loc.located
-  | CWith_Definition of identifier list Loc.located * constr_expr
-
-type module_ast =
-  | CMident of qualid Loc.located
-  | CMapply of Loc.t * module_ast * module_ast
-  | CMwith of Loc.t * module_ast * with_declaration_ast
-
 (* Returns the ranges of locs of the notation that are not occupied by args  *)
 (* and which are then occupied by proper symbols of the notation (or spaces) *)