diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index d9a82a413..f8f8c9ad2 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -854,8 +854,8 @@ let cache_notation o = load_notation 1 o; open_notation 1 o -let subst_notation (_,subst,(lc,scope,(metas,pat),b,ndf)) = - (lc,scope,(metas,subst_aconstr subst (List.map fst metas) pat),b,ndf) +let subst_notation (_,subst,(lc,scope,pat,b,ndf)) = + (lc,scope,subst_interpretation subst pat,b,ndf) let classify_notation (_,(local,_,_,_,_ as o)) = if local then Dispose else Substitute o |