diff options
| author | Pierre-Marie Pédrot | 2015-12-27 13:54:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-27 14:03:59 +0100 |
| commit | cbd815a289db52f58235f23f5afba3be49cc8eed (patch) | |
| tree | 3e75c7e36206be429ad3f81b9551d02865599eeb /kernel | |
| parent | 77e6eda6388aba117476f6c8445c4b61ebdbc33e (diff) | |
Removing dead code.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cemitcodes.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 6 |
3 files changed, 2 insertions, 10 deletions
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 |