diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 09:55:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 09:55:07 +0000 |
| commit | 4cb17c94cfb954b685f9f7ee2016e1673c640c30 (patch) | |
| tree | bd86a6402298bb70d41ccef53bd6ebac99a7f1f2 /toplevel | |
| parent | 72facd6b5e56c581f4c560a487ca40876cde12d7 (diff) | |
Bug (cf #892)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6403 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -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 a17d44666..ed9845ec4 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 |