summaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/reduction.ml')
-rw-r--r--kernel/reduction.ml8
1 files changed, 0 insertions, 8 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4153b323..b09367dd 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -28,14 +28,6 @@ open Esubst
let left2right = ref false
-let conv_key k =
- match k with
- VarKey id ->
- VarKey id
- | ConstKey (cst,_) ->
- ConstKey cst
- | RelKey n -> RelKey n
-
let rec is_empty_stack = function
[] -> true
| Zupdate _::s -> is_empty_stack s