From ef316e533fdd5f3ea599c958551707c9d75aab97 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 7 Apr 2006 20:20:16 +0000 Subject: Finalement, scopes utiles pour option 'where' (cf bug #1132) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8689 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/command.ml | 11 +++++++---- 1 file 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 -- cgit v1.2.3