diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 9f8bbad25..b103b8382 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -323,8 +323,9 @@ let interp_mutual lparams lnamearconstrs finite = let fs = States.freeze() in (* Declare the notations for the inductive types pushed in local context*) try - List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) - Metasyntax.add_notation_interpretation df ind_impls c None) notations; + List.iter (fun (df,c,scope) -> + silently (Metasyntax.add_notation_interpretation df ind_impls c) scope) + notations; let ind_env_params = push_rel_context params ind_env in let mispecvec = @@ -481,8 +482,10 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) let fs = States.freeze() in let def = try - List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) - Metasyntax.add_notation_interpretation df rec_impls c None) notations; + List.iter (fun (df,c,scope) -> + silently + (Metasyntax.add_notation_interpretation df rec_impls c) scope) + notations; List.map2 (fun ((_,_,bl,_,def),_) arity -> let def = abstract_constr_expr def bl in |