Removing dead code.

4 files changed, 0 insertions, 46 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 841a89584..93feb8b46 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -28,7 +28,6 @@ open Topconstr
 open Nametab
 open Notation
 open Inductiveops
-open Misctypes
 open Decl_kinds
 
 (** constr_expr -> glob_constr translation:
@@ -298,12 +297,6 @@ let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
 
 let reset_tmp_scope env = {env with tmp_scope = None}
 
-let set_scope env = function
-  | CastConv (GSort _) -> set_type_scope env
-  | CastConv (GRef (_,ref,_) | GApp (_,GRef (_,ref,_),_)) ->
-      {env with tmp_scope = compute_scope_of_global ref}
-  | _ -> env
-
 let rec it_mkGProd loc2 env body =
   match env with
       (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body))
@@ -1299,18 +1292,6 @@ let merge_impargs l args =
       | _ -> a::l)
     l args
 
-let check_projection isproj nargs r =
-  match (r,isproj) with
-  | GRef (loc, ref, _), Some _ ->
-      (try
-	if not (Int.equal nargs 1) then
-	  user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters.");
-      with Not_found ->
-	user_err_loc
-	(loc,"",pr_global_env Id.Set.empty ref ++ str " is not a registered projection."))
-  | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.")
-  | _, None -> ()
-
 let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
@@ -1360,10 +1341,6 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let is_projection_ref env = function
-  | ConstRef c -> Environ.is_projection c env
-  | _ -> false
-
 let internalize globalenv env allow_patvar lvar c =
   let rec intern env = function
     | CRef (ref,us) as x ->
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 3df071aff..6c4d76340 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -99,10 +99,6 @@ let init_constant dir s =
   let d = "Init"::dir in
   check_required_library (coq::d); gen_constant "Coqlib" d s
 
-let logic_constant dir s =
-  let d = "Logic"::dir in
-  check_required_library (coq::d); gen_constant "Coqlib" d s
-
 let logic_reference dir s =
   let d = "Logic"::dir in
   check_required_library ("Coq"::d); gen_reference "Coqlib" d s
@@ -139,9 +135,6 @@ let logic_type_module = make_dir logic_type_module_name
 let datatypes_module_name = init_dir@["Datatypes"]
 let datatypes_module = make_dir datatypes_module_name
 
-let arith_module_name = arith_dir@["Arith"]
-let arith_module = make_dir arith_module_name
-
 let jmeq_module_name = [coq;"Logic";"JMeq"]
 let jmeq_module = make_dir jmeq_module_name
 
@@ -273,9 +266,6 @@ let build_coq_eq_data () =
   trans = Lazy.force coq_eq_trans;
   congr = Lazy.force coq_eq_congr }
 
-let make_dirpath dir = 
-  Names.make_dirpath (List.map id_of_string dir)
-
 let build_coq_eq () = Lazy.force coq_eq_eq
 let build_coq_eq_refl () = Lazy.force coq_eq_refl
 let build_coq_eq_sym () = Lazy.force coq_eq_sym
diff --git a/interp/notation.ml b/interp/notation.ml
index 6fd6001f4..ec82c8aea 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -214,18 +214,6 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of kernel_name
 
-let compare_interp_rule x y =
-  match x, y with
-  | NotationRule (sno1, n1), NotationRule (sno2, n2) ->
-      (match sno1, sno2 with
-      | None, None -> String.compare n1 n2
-      | None, Some _ -> -1
-      | Some sn1, Some sn2 -> String.compare sn1 sn2
-      | Some _, None -> 1)
-  | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2
-  | NotationRule _, SynDefRule _ -> -1
-  | SynDefRule _, NotationRule _ -> 1
-
 (* We define keys for glob_constr and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a023462b7..524f6d743 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -82,7 +82,6 @@ let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
 let declare_syntactic_definition local id onlyparse pat =
   let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
 
-let pr_global r = pr_global_env Id.Set.empty r
 let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
 
 let allow_compat_notations = ref true