aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-05-24 16:05:02 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-05-24 16:05:02 +0200
commit71ee5fcd23c3585801e7c7534171e2af3fd939ce (patch)
tree778c93a623800d752da172f1c79e0af7841d9c1d /interp/notation.ml
parente43b85c925c0c9c87e1dde69760d9ea343c5cfa8 (diff)
parent5ec974962c7be7a7280a8094da733e32c232f5e0 (diff)
Merge PR #7177: Unifying names of "smart" combinators + adding combinators in CArray
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index e6df7b96c..192c477be 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -741,7 +741,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
match subst_scope_class subst cl with
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
- let cls' = List.smartmap subst_cl cls in
+ let cls' = List.Smart.map subst_cl cls in
(ArgsScopeNoDischarge,r',n,scl,cls')
let discharge_arguments_scope (_,(req,r,n,l,_)) =