diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-27 13:54:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-27 14:03:59 +0100 |
| commit | cbd815a289db52f58235f23f5afba3be49cc8eed (patch) | |
| tree | 3e75c7e36206be429ad3f81b9551d02865599eeb /kernel/uGraph.ml | |
| parent | 77e6eda6388aba117476f6c8445c4b61ebdbc33e (diff) | |
Removing dead code.
Diffstat (limited to 'kernel/uGraph.ml')
| -rw-r--r-- | kernel/uGraph.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 9e8ffbc7f..925b2248d 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 |