From 33b5074f24270c202a9922f21d445c12cc6b3b3d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 May 2018 13:34:46 +0200 Subject: Collecting List.smart_* functions into a module List.Smart. --- checker/declarations.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/declarations.ml') diff --git a/checker/declarations.ml b/checker/declarations.ml index ca31e143f..3368d68f7 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -513,7 +513,7 @@ let subst_decl_arity f g sub ar = let subst_rel_declaration sub = Term.map_rel_decl (subst_mps sub) -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) +let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub) let constant_is_polymorphic cb = match cb.const_universes with -- cgit v1.2.3