diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 13:34:46 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-23 18:50:10 +0200 |
commit | 33b5074f24270c202a9922f21d445c12cc6b3b3d (patch) | |
tree | 67d69b51caf3b7849e2d90d21e6ed7dc705d3249 /interp/notation.ml | |
parent | 944f62d08b7d78bcb20dd12ba138891d432b5987 (diff) |
Collecting List.smart_* functions into a module List.Smart.
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 2 |
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,_)) = |