From cbd815a289db52f58235f23f5afba3be49cc8eed Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Dec 2015 13:54:18 +0100
Subject: Removing dead code.

---
 kernel/cemitcodes.ml | 4 ----
 kernel/inductive.ml  | 2 +-
 kernel/uGraph.ml     | 6 +-----
 3 files changed, 2 insertions(+), 10 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 5ba93eda05..61042ccc17 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -306,8 +306,6 @@ let init () =
 
 type emitcodes = string
 
-let copy = String.copy
-
 let length = String.length
 
 type to_patch = emitcodes * (patch list) * fv
@@ -332,8 +330,6 @@ let subst_patch s (ri,pos) =
 let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
 
-let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
-
 type body_code =
   | BCdefined of to_patch
   | BCalias of Names.constant
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 632b4daeae..d0df5c7b38 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -151,7 +151,7 @@ let remember_subst u subst =
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env =
+let make_subst env =
   let rec make subst = function
     | (_,Some _,_)::sign, exp, args ->
         make subst (sign, exp, args)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9e8ffbc7f2..925b2248d8 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -139,7 +139,6 @@ let rec repr g u =
     | Equiv v -> repr g v
     | Canonical arc -> arc
 
-let get_prop_arc g = repr g Level.prop
 let get_set_arc g = repr g Level.set
 let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
@@ -155,7 +154,7 @@ let use_index g u =
 
 (* [safe_repr] is like [repr] but if the graph doesn't contain the
    searched universe, we add it. *)
-let rec safe_repr g u =
+let safe_repr g u =
   let rec safe_repr_rec entries u =
     match UMap.find u entries with
     | Equiv v -> safe_repr_rec entries v
@@ -745,9 +744,6 @@ let check_constraints c g =
 
 (* Normalization *)
 
-let lookup_level u g =
-  try Some (UMap.find u g) with Not_found -> None
-
 (** [normalize_universes g] returns a graph where all edges point
     directly to the canonical representent of their target. The output
     graph should be equivalent to the input graph from a logical point
-- 
cgit v1.2.3