Possibilité de syntaxe conjointement à la définition des inductifs et des points-fixes; prise en compte par le traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4042 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 181 insertions, 132 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5b88cee39e..4865611a69 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -140,6 +140,10 @@ GEXTEND Gram
   ident_comma_list_tail:
     [ [ ","; nal = LIST1 base_ident SEP "," -> nal | -> [] ] ]
   ;
+  decl_notation:
+    [ [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc] -> 
+        (ntn,scopt) ] ]
+  ;
   type_option:
     [ [ ":"; c = constr -> c 
       | -> evar_constr loc ] ]
@@ -216,9 +220,9 @@ GEXTEND Gram
           (id,c,lc) ] ]
   ;
   oneind:
-    [ [ ntn = OPT [ ntn = STRING; ":=" -> (ntn,None) ];
-        id = base_ident; indpar = simple_binders_list; ":"; c = constr; ":=";
-	lc = constructor_list -> (id,ntn,indpar,c,lc) ] ]
+    [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; 
+        ntn = OPT decl_notation ; ":="; lc = constructor_list ->
+	  (id,ntn,indpar,c,lc) ] ]
   ;
   simple_binders_list:
     [ [ bl = ne_simple_binders_list -> bl
@@ -241,12 +245,12 @@ GEXTEND Gram
   ;
   onerec:
     [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
-        ":="; def = constr ->
+        ntn = OPT decl_notation; ":="; def = constr ->
           let ni = List.length (List.flatten (List.map fst bl)) - 1 in
           let loc0 = fst (List.hd (fst (List.hd bl))) in
           let loc1 = join_loc loc0 (constr_loc type_) in
           let loc2 = join_loc loc0 (constr_loc def) in
-	  (id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+	  ((id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
   ;
   specifrec:
     [ [ l = LIST1 onerec SEP "with" -> l ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 4c62250d23..93de5a0e63 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -171,11 +171,15 @@ GEXTEND Gram
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
       | -> None ] ]
   ;
+  decl_notation:
+    [ [ OPT [ "as"; ntn = STRING; scopt = OPT [ ":"; sc = IDENT -> sc]
+               -> (ntn,scopt) ] ] ]
+    ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ ntn = OPT [ ntn = STRING -> (ntn,None) ];
-        id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; ":=";
-	lc = constructor_list -> (id,ntn,indpar,c,lc) ] ]
+    [ [ id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; 
+        ntn = decl_notation; ":="; lc = constructor_list ->
+	  (id,ntn,indpar,c,lc) ] ]
   ;
   constructor_list:
     [ [ "|"; l = LIST1 constructor_binder SEP "|" -> l
@@ -194,7 +198,8 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = base_ident; bl = LIST1 binder_nodef;
-        annot = OPT rec_annotation; type_ = type_cstr; ":="; def = lconstr ->
+        annot = OPT rec_annotation; type_ = type_cstr; 
+	ntn = decl_notation; ":="; def = lconstr ->
           let names = List.map snd (List.flatten (List.map fst bl)) in
           let ni =
             match annot with
@@ -212,7 +217,7 @@ GEXTEND Gram
           let loc0 = fst (List.hd (fst (List.hd bl))) in
           let loc1 = join_loc loc0 (constr_loc type_) in
           let loc2 = join_loc loc0 (constr_loc def) in
-	  (id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+	  ((id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)),ntn) ] ]
   ;
   corec_definition:
     [ [ id = base_ident; bl = LIST0 binder_nodef; c = type_cstr; ":=";
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d9418f58f6..11b697165c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -219,7 +219,7 @@ let interp_mutual lparams lnamearconstrs finite =
       option_app (fun df ->
         let larnames =
 	  List.rev_append lparnames 
-	    (List.map fst (fst (decompose_prod ar))) in
+	    (List.rev (List.map fst (fst (decompose_prod ar)))) in
 	(recname,larnames,df)) ntnopt)
       lnamearconstrs arityl in
   let fs = States.freeze() in
@@ -227,7 +227,7 @@ let interp_mutual lparams lnamearconstrs finite =
   try
   List.iter (option_iter (fun (recname,larnames,(df,scope)) ->
     Metasyntax.add_notation_interpretation df
-      (AVar recname,larnames) scope)) notations;
+      (AVar recname,larnames) (* no scope for tmp ntn *) scope)) notations;
   let ind_env_params = push_rel_context params ind_env in
   let mispecvec = 
     List.map2
@@ -332,33 +332,49 @@ let collect_non_rec env =
   searchrec [] 
 
 let build_recursive lnameargsardef =
-  let lrecnames = List.map (fun (f,_,_,_) -> f) lnameargsardef 
+  let lrecnames = List.map (fun ((f,_,_,_),_) -> f) lnameargsardef 
   and sigma = Evd.empty
   and env0 = Global.env()
-  and nv = Array.of_list (List.map (fun (_,n,_,_) -> n) lnameargsardef) in
+  and nv = Array.of_list (List.map (fun ((_,n,_,_),_) -> n) lnameargsardef) in
   let fs = States.freeze() in
+  (* Declare the notations for the inductive types pushed in local context*)
   let (rec_sign,arityl) = 
-    try 
-      List.fold_left 
-        (fun (env,arl) (recname,_,arityc,_) -> 
-           let arity = interp_type sigma env0 arityc in
-           let _ = declare_variable recname
-	     (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
-           (Environ.push_named (recname,None,arity) env, (arity::arl)))
-        (env0,[]) lnameargsardef
-    with e ->
-      States.unfreeze fs; raise e in
+    List.fold_left 
+      (fun (env,arl) ((recname,_,arityc,_),_) -> 
+        let arity = interp_type sigma env0 arityc in
+        (Environ.push_named (recname,None,arity) env, (arity::arl)))
+      (env0,[]) lnameargsardef in
   let arityl = List.rev arityl in
+  let notations = 
+    List.map2 (fun ((recname,_,_,_),ntnopt) arityl ->
+      option_app (fun ntn ->
+        let larnames = List.map fst (fst (decompose_prod arityl)) in
+	(recname,List.rev larnames,ntn)) ntnopt)
+      lnameargsardef arityl in
+
   let recdef =
-    try 
-      List.map2
-	(fun (_,_,_,def) arity ->
-          interp_casted_constr sigma rec_sign def arity)
-        lnameargsardef arityl
-    with e ->
-      States.unfreeze fs; raise e
+
+    (* Declare local context and local notations *)
+    let fs = States.freeze() in
+    let def = 
+      try
+	List.iter (option_iter (fun (recname,larnames,(df,scope)) ->
+	  Metasyntax.add_notation_interpretation df
+	  (AVar recname,larnames) (* no scope for tmp ntn *) None)) notations;
+	List.iter2
+	  (fun recname arity -> 
+            let _ = declare_variable recname
+	      (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
+	    ()) lrecnames arityl;
+	List.map2
+	  (fun ((_,_,_,def),_) arity ->
+            interp_casted_constr sigma rec_sign def arity)
+          lnameargsardef arityl
+      with e ->
+	States.unfreeze fs; raise e in
+    States.unfreeze fs; def 
   in
-  States.unfreeze fs;
+
   let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
     collect_non_rec env0 lrecnames recdef arityl (Array.to_list nv) in
   let recvec = 
@@ -389,7 +405,9 @@ let build_recursive lnameargsardef =
       (List.map var_subst (Array.to_list namerec))
       lnonrec 
   in
-  ()
+  List.iter (option_iter (fun (recname,names,(df,scope)) ->
+      Metasyntax.add_notation_interpretation df
+        (ARef (ConstRef (Lib.make_kn recname)),names) scope)) notations
 
 let build_corecursive lnameardef = 
   let lrecnames = List.map (fun (f,_,_) -> f) lnameardef
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 791c33d66a..4ed7a89288 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -43,7 +43,7 @@ val build_mutual : inductive_expr list -> bool -> unit
 val declare_mutual_with_eliminations :
   Entries.mutual_inductive_entry -> mutual_inductive
 
-val build_recursive : fixpoint_expr list -> unit
+val build_recursive : (fixpoint_expr * decl_notation) list -> unit
 
 val build_corecursive : cofixpoint_expr list -> unit
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 1e0077373d..43785836af 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -437,35 +437,6 @@ let rec find_symbols c_current c_next c_last = function
   | Terminal s :: sl -> find_symbols c_next c_next c_last sl
   | Break n :: sl -> find_symbols c_current c_next c_last sl
 
-(*
-let rec find_symbols c_current c_next c_last = function
-  | []    -> (vars, [])
-  | String x :: sl when Lexer.is_normal_token x ->
-      Lexer.check_ident x;
-      let id = Names.id_of_string x in
-      if List.mem_assoc id vars then
-	error ("Variable "^x^" occurs more than once");
-      let prec = if sl <> [] then c_current else c_last in
-      let (vars,l) = find_symbols c_next c_next c_last sl in
-      ((id,prec)::vars, NonTerminal id :: l)
-(*
-  | "_"::sl ->
-      warning "Found '_'";
-      let prec = if List.exists is_symbols sl then c_first else c_last in
-      let (vars,l) =
-        find_symbols c_next c_next c_last vars (new_var+1) varprecl sl in
-      let meta = create_meta new_var in
-      (vars, NonTerminal (prec, meta) :: l)
-*)
-  | String s :: sl ->
-      Lexer.check_special_token s;
-      let (vars,l) = find_symbols c_next c_next c_last sl in
-      (vars, Terminal (strip s) :: l)
-  | WhiteSpace n :: sl ->
-      let (vars,l) = find_symbols c_current c_next c_last sl in
-      (vars, Break n :: l)
-*)
-
 let make_grammar_rule n assoc typs symbols ntn =
   let prod = make_production typs symbols in
   (n,assoc,ntn,prod)
@@ -546,8 +517,7 @@ let interp_modifiers a n =
   let onlyparsing = ref false in
   let rec interp assoc level etyps = function
     | [] ->
-	let n = match level with None -> 1 | Some n -> n in
-	(assoc,n,etyps,!onlyparsing)
+	(assoc,level,etyps,!onlyparsing)
     | SetEntryType (s,typ) :: l ->
 	let id = id_of_string s in
 	if List.mem_assoc id etyps then
@@ -575,16 +545,18 @@ let interp_modifiers a n =
 
 (* Infix defaults to LEFTA (cf doc) *)
 let interp_infix_modifiers a n l =
-  let (assoc,n,t,b) = interp_modifiers a n l in
+  let (assoc,level,t,b) = interp_modifiers a n l in
   if t <> [] then
     error "explicit entry level or type unexpected in infix notation";
   let assoc = match assoc with None -> Some Gramext.LeftA | a -> a in
+  let n = match level with None -> 1 | Some n -> n in
   (assoc,n,b)
 
 (* Notation defaults to NONA *)
 let interp_notation_modifiers modl =
   let (assoc,n,t,b) = interp_modifiers None None modl in
   let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
+  let n = match n with None -> 1 | Some n -> n in
   (assoc,n,t,b)
 
 (* 2nd list of types has priority *)
@@ -761,54 +733,88 @@ let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks =
   Lib.add_anonymous_leaf
     (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,df))
 
-let add_notation local df a modifiers mv8 sc =
-  let toks = split df in
-  match toks with 
-    | [String x] when quote(strip x) = x
-	& (modifiers = [] or modifiers = [SetOnlyParsing]) ->
-        (* Means a Syntactic Definition *)
-        let ident = id_of_string (strip x) in
-	let c = snd (interp_aconstr [] a) in
-	let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
-        Syntax_def.declare_syntactic_definition local ident onlyparse c
-    | _ ->
-        add_notation_in_scope local
-          df a (interp_notation_modifiers modifiers)
-          (option_app (fun (s8,ml8) ->
-            let toks8 = split s8 in 
-            let im8 = interp_notation_modifiers ml8 in
-            (toks8,im8)) mv8)
-          sc toks
-
-let check_occur l id =
-  if not (List.mem (Name id) l) then error ((string_of_id id)^"is unbound")
-
-let add_notation_interpretation df (c,l) sc =
+let add_notation_interpretation_core local vars symbs df (a,r) sc onlyparse =
   let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
-  let (vars,symbs) = analyse_tokens (split df) in
   let notation = make_anon_notation symbs in
   let prec = 
     try Symbols.level_of_notation notation
     with Not_found ->
       error "Parsing rule for this notation has to be previously declared" in
-  List.iter (check_occur l) vars;
   let old_pp_rule =
-    let c = match c with AVar id -> RVar (dummy_loc,id)
-      | ARef c -> RRef (dummy_loc,c)
-      | _ -> anomaly "add_notation_interpretation" in
     let typs = List.map2 
       (fun id n -> id,ETConstr (NumLevel n,InternalProd)) vars (snd prec) in
-    let r = RApp (dummy_loc, c,
-    List.map (function Name id when List.mem id vars -> RVar (dummy_loc,id)
-      | _ -> RHole (dummy_loc,QuestionMark)) l) in
     Some (make_old_pp_rule (fst prec) symbs typs r notation scope vars) in
-  let a = AApp (c,List.map (function Name id when List.mem id vars -> AVar id | 
-_ -> AHole QuestionMark) l) in
+  Lib.add_anonymous_leaf
+    (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,df))
+
+let check_occur l id =
+  if not (List.mem (Name id) l) then error ((string_of_id id)^"is unbound")
+
+let add_notation_interpretation df (c,l) sc =
+  let (vars,symbs) = analyse_tokens (split df) in
+  List.iter (check_occur l) vars;
+  let a_for_old =
+    let c = match c with AVar id -> RVar (dummy_loc,id)
+      | ARef c -> RRef (dummy_loc,c)
+      | _ -> anomaly "add_notation_interpretation" in
+    RApp (dummy_loc, c,
+      List.map (function
+	| Name id when List.mem id vars -> RVar (dummy_loc,id)
+	| _ -> RHole (dummy_loc,QuestionMark)) l) in
+  let a = AApp (c,List.map (function 
+    | Name id when List.mem id vars -> AVar id
+    | _ -> AHole QuestionMark) l) in
   let la = List.map (fun id -> id,[]) vars in
   let onlyparse = false in
   let local = false in
-  Lib.add_anonymous_leaf
-    (inNotation(local,old_pp_rule,notation,scope,(la,a),onlyparse,df))
+  add_notation_interpretation_core local vars symbs df ((la,a),a_for_old) sc
+    onlyparse
+
+let add_notation local df c modifiers mv8 sc =
+  let toks = split df in
+  match toks with 
+    | [String x] when quote(strip x) = x
+	(* This is an ident that can be qualified: a syntactic definition *)
+	& (modifiers = [] or modifiers = [SetOnlyParsing]) ->
+        (* Means a Syntactic Definition *)
+        let ident = id_of_string (strip x) in
+	let c = snd (interp_aconstr [] c) in
+	let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
+        Syntax_def.declare_syntactic_definition local ident onlyparse c
+    | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
+	(* This is a ident to be declared as a rule *)
+        add_notation_in_scope local df c (None,0,[],modifiers=[SetOnlyParsing])
+          (option_app (fun (s8,ml8) ->
+	    let toks8 = split s8 in 
+	    let im8 = interp_notation_modifiers ml8 in
+	    (toks8,im8)) mv8)
+        sc toks
+    | _ ->
+	let (assoc,lev,typs,onlyparse) = interp_modifiers None None modifiers
+	in
+	match lev with
+	  | None->
+	      if modifiers <> [] & modifiers <> [SetOnlyParsing] then
+		error "Parsing rule for this notation includes no level"
+	      else
+	        (* Declare only interpretation *)
+		let (vars,symbs) = analyse_tokens toks in
+		let onlyparse = modifiers = [SetOnlyParsing] in
+		let a = interp_aconstr vars c in
+		let a_for_old = interp_rawconstr_gen
+		  false Evd.empty (Global.env()) [] (Some []) (vars,[]) c in
+		add_notation_interpretation_core local vars symbs df
+		  (a,a_for_old) sc onlyparse
+	  | Some n ->
+	    (* Declare both syntax and interpretation *)
+	    let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
+	    let mods = (assoc,n,typs,onlyparse)	in
+            add_notation_in_scope local df c mods
+              (option_app (fun (s8,ml8) ->
+		let toks8 = split s8 in 
+		let im8 = interp_notation_modifiers ml8 in
+		(toks8,im8)) mv8)
+              sc toks
 
 (* TODO add boxes information in the expression *)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index dea54e58a2..b52af04f3a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -140,13 +140,15 @@ let rec vernac_com interpfun (loc,com) =
              Options.v7_only := true;
              if !translate_file then msg (pr_comments !comments)
          | _ ->
+	     let fs = States.freeze () in
              if !translate_file then
                msgnl
 		 (pr_comments !comments ++ hov 0 (pr_vernac com) ++ sep_end())
              else
-	       msgnl
+	       (msgnl
                  (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++
-                         pr_vernac com ++ sep_end())));
+                         pr_vernac com ++ sep_end()));
+		 States.unfreeze fs));
        Constrintern.set_temporary_implicits_in [];
        Constrextern.set_temporary_implicits_out [];
        comments := None;
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index b68fe70225..7388137720 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -177,7 +177,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
   | VernacInductive of inductive_flag * inductive_expr list
-  | VernacFixpoint of fixpoint_expr list
+  | VernacFixpoint of (fixpoint_expr * decl_notation) list
   | VernacCoFixpoint of cofixpoint_expr list
   | VernacScheme of (identifier * bool * reference * sort_expr) list
 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 7954f17c09..da4d7928a7 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -236,6 +236,11 @@ let pr_type_option pr_c = function
   | CHole loc -> mt()
   | _ as c -> str":" ++ pr_c c
 
+let pr_decl_notation =
+  pr_opt (fun (ntn,scopt) -> 
+    str "as " ++ str (quote ntn) ++ 
+    pr_opt (fun sc -> str " :" ++ str sc) scopt)
+
 let anonymize_binder na c =
   if Options.do_translate() then
     Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env()))
@@ -487,7 +492,7 @@ let rec pr_vernac = function
         | Some ml -> ml in
       str"Uninterpreted Notation" ++ spc() ++ pr_locality local ++ qs s ++
       (match l with | [] -> mt() | _ as l -> 
-	str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+	str" (" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
   (* Gallina *)
   | VernacDefinition (d,id,b,f,e) -> (* A verifier... *)
@@ -555,8 +560,9 @@ let rec pr_vernac = function
 	    (Termops.push_rel_assum (Name id,p) env,
 	    (Name id,None,p)::params))
 	  (env0,[]) lparams in
-      let impls = List.map
-	(fun (recname,_,_,arityc,_) ->
+      let lparnames = List.map (fun (na,_,_) -> na) params in
+      let impl_ntns = List.map
+	(fun (recname,ntnopt,_,arityc,_) ->
 	  let arity = Constrintern.interp_type sigma env_params arityc in
 	  let fullarity =
             Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params)
@@ -569,9 +575,16 @@ let rec pr_vernac = function
 	    if Impargs.is_implicit_args_out()
 	    then Impargs.compute_implicits true env_params fullarity
 	    else [] in
-	  (recname,impl_in,impl_out)) l in
-      let impls_in = List.map (fun (id,a,_) -> (id,a)) impls in
-      let impls_out = List.map (fun (id,_,a) -> (id,a)) impls in
+	  let notation =
+	    option_app (fun df ->
+	      (List.rev_append lparnames 
+		(List.rev (List.map fst (fst (Term.decompose_prod arity)))),
+	      df))
+	      ntnopt in
+	  (recname,impl_in,impl_out,notation)) l in
+      let impls_in = List.map (fun (id,a,_,_) -> (id,a)) impl_ntns in
+      let impls_out = List.map (fun (id,_,a,_) -> (id,a)) impl_ntns in
+      let notations = List.map (fun (id,_,_,n) -> (id,n)) impl_ntns in
       Constrintern.set_temporary_implicits_in impls_in;
       Constrextern.set_temporary_implicits_out impls_out;
       (* Fin calcul implicites *)
@@ -590,24 +603,13 @@ let rec pr_vernac = function
           str key ++ spc() ++
           pr_id id ++ spc() ++ pr_sbinders indpar ++ str":" ++ spc() ++
           pr_lconstr s ++ 
-          pr_opt (fun (ntn,scopt) -> 
-	    str "as " ++ str (quote ntn) ++ 
-            pr_opt (fun sc -> str " :" ++ str sc) scopt)
-          ntn ++ str" :=") ++ pr_constructor_list lc in
+	  pr_decl_notation ntn ++ str" :=") ++ pr_constructor_list lc in
 
       (* Copie simplifiée de command.ml pour déclarer les notations locales *)
-      let lparnames = List.map (fun (na,_,_) -> na) params in
-      let notations = 
-	List.map (fun (recname,ntnopt,_,arityc,_) ->
-          let arity = Constrintern.interp_type sigma env_params arityc in
-	  option_app (fun df ->
-            let larnames =
-	      List.rev_append lparnames 
-		(List.map fst (fst (Term.decompose_prod arity))) in
-	    (recname,larnames,df)) ntnopt) l in
-      List.iter (option_iter (fun (recname,larnames,(df,scope)) ->
+      List.iter (fun (recname,no) ->
+	option_iter (fun (larnames,(df,scope)) ->
 	Metasyntax.add_notation_interpretation df
-	(AVar recname,larnames) scope)) notations;
+	(AVar recname,larnames) scope) no) notations;
 
       hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l))
       ++ 
@@ -619,8 +621,8 @@ let rec pr_vernac = function
       (* Copie simplifiée de command.ml pour recalculer les implicites *)
       let sigma = Evd.empty
       and env0 = Global.env() in
-      let impls = List.map
-        (fun (recname,_,arityc,_) -> 
+      let impl_ntns = List.map
+        (fun ((recname,_,arityc,_),ntnopt) -> 
           let arity = Constrintern.interp_type sigma env0 arityc in
 	  let impl_in =
 	    if Impargs.is_implicit_args()
@@ -630,14 +632,25 @@ let rec pr_vernac = function
 	    if Impargs.is_implicit_args_out()
 	    then Impargs.compute_implicits true env0 arity
 	    else [] in
-	  (recname,impl_in,impl_out)) recs in
-      let impls_in = List.map (fun (id,a,_) -> (id,a)) impls in
-      let impls_out = List.map (fun (id,_,a) -> (id,a)) impls in
+	  let notations = 
+	    option_app (fun ntn ->
+              let larnames = List.map fst (fst (Term.decompose_prod arity)) in
+	      (List.rev larnames,ntn)) ntnopt in
+	  (recname,impl_in,impl_out,notations)) recs in
+      let impls_in = List.map (fun (id,a,_,_) -> (id,a)) impl_ntns in
+      let impls_out = List.map (fun (id,_,a,_) -> (id,a)) impl_ntns in
+      let notations = List.map (fun (id,_,_,n) -> (id,n)) impl_ntns in
       Constrintern.set_temporary_implicits_in impls_in;
       Constrextern.set_temporary_implicits_out impls_out;
 
+      (* Copie simplifiée de command.ml pour déclarer les notations locales *)
+      List.iter (fun (recname,no) ->
+	option_iter (fun (larnames,(df,scope)) ->
+	Metasyntax.add_notation_interpretation df
+	(AVar recname,larnames) scope) no) notations;
+
       let pr_onerec = function
-        | (id,n,type_0,def0) ->
+        | (id,n,type_0,def0),ntn ->
             let (bl,def,type_) = extract_def_binders def0 type_0 in
             let ids = List.flatten (List.map fst bl) in
             let (bl,def,type_) =
@@ -651,7 +664,8 @@ let rec pr_vernac = function
               else mt() in
             pr_id id ++ str" " ++ pr_binders bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr c) type_
-            ++ str" :=" ++ brk(1,1) ++ pr_lconstr def in
+            ++ pr_decl_notation ntn ++ str" :=" ++ brk(1,1) ++ pr_lconstr def
+      in
       hov 1 (str"Fixpoint" ++ spc() ++
         prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)