aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/redexpr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6fb411938..a75711bae 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -92,9 +92,9 @@ let cache_strategy (_,str) =
let subst_strategy (subs,(local,obj)) =
local,
- List.smartmap
+ List.Smart.map
(fun (k,ql as entry) ->
- let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+ let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
if ql==ql' then entry else (k,ql'))
obj