diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-07 20:20:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-07 20:20:16 +0000 |
| commit | ef316e533fdd5f3ea599c958551707c9d75aab97 (patch) | |
| tree | 7eea6e4bce2f3020c516061d25eefeb20d181a44 | |
| parent | 26ca22424b286f5ff22a1fa97c38d15e224b3dc2 (diff) | |
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
| -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 |