diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index f0cdc49cda..0628e72297 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -493,7 +493,9 @@ let cache_arguments_scope o = let subst_arguments_scope (subst,(req,r,scl,cls)) = let r' = fst (subst_global subst r) in - let cls' = list_smartmap (Option.smartmap (subst_cl_typ subst)) cls in + let subst_cl cl = + try Option.smartmap (subst_cl_typ subst) cl with Not_found -> None in + let cls' = list_smartmap subst_cl cls in let scl' = merge_scope (List.map find_class_scope_opt cls') scl in let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in (ArgsScopeNoDischarge,r',scl'',cls') |