diff options
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index a17d446660..ed9845ec45 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -491,7 +491,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) let def = try List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) - Metasyntax.add_notation_interpretation df [] c None) notations; + Metasyntax.add_notation_interpretation df rec_impls c None) notations; List.map2 (fun ((_,_,bl,_,def),_) arity -> let def = abstract_rawconstr def bl in |