diff options
| author | Pierre-Marie Pédrot | 2016-05-08 18:59:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-08 19:59:03 +0200 |
| commit | f461e7657cab9917c5b405427ddba3d56f197efb (patch) | |
| tree | 467ac699f78d0360b05174238aeb1177da892503 /kernel | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytecodes.ml | 3 | ||||
| -rw-r--r-- | kernel/names.ml | 2 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 1 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 1 | ||||
| -rw-r--r-- | kernel/reduction.ml | 1 | ||||
| -rw-r--r-- | kernel/vconv.ml | 4 |
6 files changed, 1 insertions, 11 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index f9cf2691ee..a705e3004f 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -184,9 +184,6 @@ let rec pp_struct_const = function let pp_lbl lbl = str "L" ++ int lbl -let pp_pcon (id,u) = - pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}" - let pp_fv_elem = function | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")" | FVrel i -> str "Rel(" ++ int i ++ str ")" diff --git a/kernel/names.ml b/kernel/names.ml index 8e0237863f..e8226d3d32 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -341,7 +341,7 @@ module ModPath = struct | MPfile dir -> MPfile (hdir dir) | MPbound m -> MPbound (huniqid m) | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l) - let rec eq d1 d2 = + let eq d1 d2 = d1 == d2 || match d1,d2 with | MPfile dir1, MPfile dir2 -> dir1 == dir2 diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 7ac5b8d7b2..4ed926f1fe 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors open Names -open Univ open Nativelib open Reduction open Util diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 0e56e76aa5..c307896416 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,7 +15,6 @@ open Util open Names -open Univ open Term open Declarations open Context.Named.Declaration diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f23ed16f05..5bf369441f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -20,7 +20,6 @@ open Util open Names open Term open Vars -open Univ open Environ open Closure open Esubst diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 4610dbcb07..89e833254a 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -1,13 +1,9 @@ open Util open Names -open Term open Environ -open Conv_oracle open Reduction -open Closure open Vm open Csymtable -open Univ let val_of_constr env c = val_of_constr (pre_env env) c |