From 4cb17c94cfb954b685f9f7ee2016e1673c640c30 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 09:55:07 +0000
Subject: Bug (cf #892)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6403 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3