aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-23 13:34:46 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-23 18:50:10 +0200
commit33b5074f24270c202a9922f21d445c12cc6b3b3d (patch)
tree67d69b51caf3b7849e2d90d21e6ed7dc705d3249 /kernel/context.ml
parent944f62d08b7d78bcb20dd12ba138891d432b5987 (diff)
Collecting List.smart_* functions into a module List.Smart.
Diffstat (limited to 'kernel/context.ml')
-rw-r--r--kernel/context.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/context.ml b/kernel/context.ml
index 4f3f649c1..5d4a10184 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -192,7 +192,7 @@ struct
let equal eq l = List.equal (fun c -> Declaration.equal eq c) l
(** Map all terms in a given rel-context. *)
- let map f = List.smartmap (Declaration.map_constr f)
+ let map f = List.Smart.map (Declaration.map_constr f)
(** Perform a given action on every declaration in a given rel-context. *)
let iter f = List.iter (Declaration.iter_constr f)
@@ -392,7 +392,7 @@ struct
let equal eq l = List.equal (fun c -> Declaration.equal eq c) l
(** Map all terms in a given named-context. *)
- let map f = List.smartmap (Declaration.map_constr f)
+ let map f = List.Smart.map (Declaration.map_constr f)
(** Perform a given action on every declaration in a given named-context. *)
let iter f = List.iter (Declaration.iter_constr f)