aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/redexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/redexpr.ml')
-rw-r--r--proofs/redexpr.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index be92f2b04..89ecdb0df 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -158,8 +158,6 @@ let make_flag env f =
f.rConst red
in red
-let is_reference = function PRef _ | PVar _ -> true | _ -> false
-
(* table of custom reductino fonctions, not synchronized,
filled via ML calls to [declare_reduction] *)
let reduction_tab = ref String.Map.empty