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, 1 insertions, 1 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index c7d6ffe14..2e10a9f4a 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -77,7 +77,7 @@ let export_strategy (local,obj) =
EvalVarRef _ -> None
| EvalConstRef _ as q -> Some q) obj
-let classify_strategy (_,(local,_ as obj)) =
+let classify_strategy (local,_ as obj) =
if local then Dispose else Substitute obj
let disch_ref ref =