Extension of the recursive notations mechanism

- Added support for recursive notations with binders
- Added support for arbitrary large iterators in recursive notations
- More checks on the use of variables and improved error messages
- Do side-effects in metasyntax only when sure that everything is ok
- Documentation

Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).

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

11 files changed, 119 insertions, 64 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index a32bfdec4..db28c866f 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -62,44 +62,53 @@ type grammar_constr_prod_item =
     (* tells action rule to make a list of the n previous parsed items; 
        concat with last parsed list if true *)
 
-type 'a action_env = 'a list * 'a list list
-
 let make_constr_action
-  (f : loc -> constr_expr action_env -> constr_expr) pil =
-  let rec make (env,envlist as fullenv : constr_expr action_env) = function
+  (f : loc -> constr_notation_substitution -> constr_expr) pil =
+  let rec make (constrs,constrlists,binders as fullsubst) = function
   | [] ->
-      Gram.action (fun loc -> f loc fullenv)
+      Gram.action (fun loc -> f loc fullsubst)
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
       (* parse a non-binding item *)
-      Gram.action (fun _ -> make fullenv tl)
+      Gram.action (fun _ -> make fullsubst tl)
   | GramConstrNonTerminal (typ, Some _) :: tl ->
       (* parse a binding non-terminal *)
     (match typ with
     | (ETConstr _| ETOther _) ->
-        Gram.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
+	Gram.action (fun (v:constr_expr) ->
+	  make (v :: constrs, constrlists, binders) tl)
     | ETReference ->
-        Gram.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
+        Gram.action (fun (v:reference) ->
+	  make (CRef v :: constrs, constrlists, binders) tl)
     | ETName ->
         Gram.action (fun (na:name located) ->
-	  make (constr_expr_of_name na :: env, envlist) tl)
+	  make (constr_expr_of_name na :: constrs, constrlists, binders) tl)
     | ETBigint ->
         Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
+	  make (CPrim(dummy_loc,Numeral v) :: constrs, constrlists, binders) tl)
     | ETConstrList (_,n) ->
-	Gram.action (fun (v:constr_expr list) -> make (env, v::envlist) tl)
+	Gram.action (fun (v:constr_expr list) ->
+	  make (constrs, v::constrlists, binders) tl)
+    | ETBinder _ | ETBinderList (true,_) ->
+	Gram.action (fun (v:local_binder list) ->
+	  make (constrs, constrlists, v::binders) tl)
+    | ETBinderList (false,_) ->
+	Gram.action (fun (v:local_binder list list) ->
+	  make (constrs, constrlists, List.flatten v::binders) tl)
     | ETPattern ->
 	failwith "Unexpected entry of type cases pattern")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
-      let heads,env = list_chop n env in
-      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
-      else make (env,heads::envlist) tl
+      let heads,constrs = list_chop n constrs in
+      let constrlists =
+	if b then (heads@List.hd constrlists)::List.tl constrlists
+	else heads::constrlists
+      in make (constrs, constrlists, binders) tl
   in
-  make ([],[]) (List.rev pil)
+  make ([],[],[]) (List.rev pil)
 
 let make_cases_pattern_action
-  (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil =
-  let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function
+  (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
+  let rec make (env,envlist as fullenv) = function
   | [] ->
       Gram.action (fun loc -> f loc fullenv)
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
@@ -122,7 +131,7 @@ let make_cases_pattern_action
     | ETConstrList (_,_) ->
         Gram.action  (fun (vl:cases_pattern_expr list) ->
 	  make (env, vl :: envlist) tl)
-    | (ETPattern | ETOther _) ->
+    | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
 	failwith "Unexpected entry of type cases pattern or other")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
@@ -273,7 +282,10 @@ type notation_grammar =
     int * gram_assoc option * notation * grammar_constr_prod_item list list
 
 type all_grammar_command =
-  | Notation of (precedence * tolerability list) * notation_grammar
+  | Notation of
+	 (precedence * tolerability list) *
+	  notation_var_internalization_type list *
+	  notation_grammar
   | TacticGrammar of
       (string * int * grammar_prod_item list *
          (dir_path * Tacexpr.glob_tactic_expr))
@@ -282,14 +294,16 @@ let (grammar_state : all_grammar_command list ref) = ref []
 
 let extend_grammar gram =
   (match gram with
-  | Notation (_,a) -> extend_constr_notation a
+  | Notation (_,_,a) -> extend_constr_notation a
   | TacticGrammar g -> add_tactic_entry g);
   grammar_state := gram :: !grammar_state
 
 let recover_notation_grammar ntn prec =
   let l = map_succeed (function
-    | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x
-    | _ -> failwith "") !grammar_state in
+    | Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
+	 vars, x
+    | _ ->
+	 failwith "") !grammar_state in
   assert (List.length l = 1);
   List.hd l
 
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 56e6b1d61..05b2ddd99 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -45,7 +45,12 @@ type grammar_prod_item =
 (** Adding notations *)
 
 type all_grammar_command =
-  | Notation of (precedence * tolerability list) * notation_grammar
+  | Notation of
+	 (precedence * tolerability list)
+	  * notation_var_internalization_type list
+	   (** not needed for defining grammar, hosted by egrammar for
+	       transmission to interp_aconstr (via recover_notation_grammar) *)
+	  * notation_grammar
   | TacticGrammar of
       (string * int * grammar_prod_item list *
          (dir_path * Tacexpr.glob_tactic_expr))
@@ -61,5 +66,8 @@ val extend_vernac_command_grammar :
 val get_extend_vernac_grammars :
  unit -> (string * grammar_prod_item list list) list
 
+(** For a declared grammar, returns the rule + the ordered entry types
+    of variables in the rule (for use in the interpretation) *)
 val recover_notation_grammar :
-  notation -> (precedence * tolerability list) -> notation_grammar
+  notation -> (precedence * tolerability list) ->
+  notation_var_internalization_type list * notation_grammar
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 4674a7c90..f7daafb03 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -23,17 +23,19 @@ type production_level =
 
 type ('lev,'pos) constr_entry_key_gen =
   | ETName | ETReference | ETBigint
+  | ETBinder of bool (* true=open, as in "fun .."; false as in "let f .. :=" *)
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
   | ETConstrList of ('lev * 'pos) * Tok.t list
+  | ETBinderList of bool * Tok.t list
 
 (**  Entries level (left-hand-side of grammar rules) *)
 
 type constr_entry_key =
     (int,unit) constr_entry_key_gen
 
-(** Entries used in productions (in right-hand-side of grammar rules) *)
+(** Entries used in productions (in right-hand side of grammar rules) *)
 
 type constr_prod_entry_key =
     (production_level,production_position) constr_entry_key_gen
diff --git a/parsing/extend.mli b/parsing/extend.mli
index a05952294..fa2fef6b5 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -22,10 +22,12 @@ type production_level =
 
 type ('lev,'pos) constr_entry_key_gen =
   | ETName | ETReference | ETBigint
+  | ETBinder of bool
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
   | ETConstrList of ('lev * 'pos) * Tok.t list
+  | ETBinderList of bool * Tok.t list
 
 (** Entries level (left-hand-side of grammar rules) *)
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e3c898284..f74d28f0b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -31,11 +31,6 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
 
-let loc_of_binder = function
-  | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc
-  | LocalRawDef ((loc,_),_)::_ -> loc
-  | _ -> dummy_loc
-
 let binders_of_lidents l =
   List.map (fun (loc, id) ->
     LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
@@ -129,7 +124,7 @@ let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  closed_binder binders binders_fixannot
+  closed_binder open_binders binder binders binders_fixannot
   record_declaration typeclass_constraint pattern appl_arg;
   Constr.ident:
     [ [ id = Prim.ident -> id
@@ -202,7 +197,7 @@ GEXTEND Gram
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c with
               CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CNotation(loc,"( _ )",([c],[]))
+                CNotation(loc,"( _ )",([c],[],[]))
             | _ -> c)
       | "{|"; c = record_declaration; "|}" -> c
       | "`{"; c = operconstr LEVEL "200"; "}" ->
@@ -238,7 +233,7 @@ GEXTEND Gram
           mkCLambdaN loc bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-          let loc1 = loc_of_binder bl in
+          let loc1 = join_loc (local_binders_loc bl) (constr_loc c1) in
           CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
@@ -392,12 +387,15 @@ GEXTEND Gram
     (* Same as binders but parentheses around a closed binder are optional if
        the latter is unique *)
     [ [ (* open binder *)
-        idl = LIST1 name; ":"; c = lconstr ->
-          [LocalRawAssum (idl,Default Explicit,c)]
+        id = name; idl = LIST0 name; ":"; c = lconstr ->
+          [LocalRawAssum (id::idl,Default Explicit,c)]
 	(* binders factorized with open binder *)
-      | idl = LIST1 name; bl = binders ->
-          let t = CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))) in
-          LocalRawAssum (idl,Default Explicit,t)::bl
+      | id = name; idl = LIST0 name; bl = binders ->
+          let t = CHole (loc, Some (Evd.BinderType (snd id))) in
+          LocalRawAssum (id::idl,Default Explicit,t)::bl
+      | id1 = name; ".."; id2 = name ->
+          [LocalRawAssum ([id1;(loc,Name ldots_var);id2],
+	                  Default Explicit,CHole (loc,None))]
       | bl = closed_binder; bl' = binders ->
 	  bl@bl'
     ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3e5a52e46..e4513e58d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -931,6 +931,8 @@ GEXTEND Gram
   syntax_extension_type:
     [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
+      | IDENT "binder" -> ETBinder true
+      | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
   opt_scope:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 3cdf89ebd..1c35a2149 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -355,7 +355,9 @@ module Constr =
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
     let closed_binder = Gram.entry_create "constr:closed_binder"
+    let binder = Gram.entry_create "constr:binder"
     let binders = Gram.entry_create "constr:binders"
+    let open_binders = Gram.entry_create "constr:open_binders"
     let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
     let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
     let record_declaration = Gram.entry_create "constr:record_declaration"
@@ -602,10 +604,15 @@ let compute_entry allow_create adjust forpat = function
        else weaken_entry Constr.operconstr),
       adjust (n,q), false
   | ETName -> weaken_entry Prim.name, None, false
+  | ETBinder true -> anomaly "Should occur only as part of BinderList"
+  | ETBinder false -> weaken_entry Constr.binder, None, false
+  | ETBinderList (true,tkl) ->
+      assert (tkl=[]); weaken_entry Constr.open_binders, None, false
+  | ETBinderList (false,_) -> anomaly "List of entries cannot be registered."
   | ETBigint -> weaken_entry Prim.bigint, None, false
   | ETReference -> weaken_entry Constr.global, None, false
   | ETPattern -> weaken_entry Constr.pattern, None, false
-  | ETConstrList _ -> error "List of entries cannot be registered."
+  | ETConstrList _ -> anomaly "List of entries cannot be registered."
   | ETOther (u,n) ->
       let u = get_univ u in
       let e =
@@ -645,6 +652,12 @@ let is_binder_level from e =
       ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true
     | _ -> false
 
+let make_sep_rules tkl =
+  Gram.srules'
+    [List.map gram_token_of_token tkl,
+     List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl
+       (Gram.action (fun loc -> ()))]
+
 let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
   if is_binder_level from typ then
     if forpat then
@@ -660,10 +673,15 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
     | ETConstrList (typ',tkl) ->
         Slist1sep
           (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
-           Gram.srules'
-             [List.map gram_token_of_token tkl,
-              List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl
-                (Gram.action (fun loc -> ()))])
+	   make_sep_rules tkl)
+    | ETBinderList (false,[]) ->
+        Slist1
+	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
+    | ETBinderList (false,tkl) ->
+        Slist1sep
+	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
+	   make_sep_rules tkl)
+
     | _ ->
     match interp_constr_prod_entry_key assoc from forpat typ with
       | (eobj,None,_) -> Snterm (Gram.Entry.obj eobj)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 99c155e8d..80f4b65fe 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -197,7 +197,9 @@ module Constr :
     val constr_pattern : constr_expr Gram.entry
     val lconstr_pattern : constr_expr Gram.entry
     val closed_binder : local_binder list Gram.entry
-    val binders : local_binder list Gram.entry
+    val binder : local_binder list Gram.entry (* closed_binder or variable *)
+    val binders : local_binder list Gram.entry (* list of binder *)
+    val open_binders : local_binder list Gram.entry
     val binders_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry
     val typeclass_constraint : (name located * bool * constr_expr) Gram.entry
     val record_declaration : constr_expr Gram.entry
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 6a4d9757d..e0a8c173a 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -62,8 +62,8 @@ let prec_of_prim_token = function
 
 open Notation
 
-let print_hunks n pr (env,envlist) unp =
-  let env = ref env and envlist = ref envlist in
+let print_hunks n pr pr_binders (terms,termlists,binders) unp =
+  let env = ref terms and envlist = ref termlists and bll = ref binders in
   let pop r = let a = List.hd !r in r := List.tl !r; a in
   let rec aux = function
   | [] -> mt ()
@@ -74,6 +74,8 @@ let print_hunks n pr (env,envlist) unp =
       let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
       let pp2 = aux l in
       pp1 ++ pp2
+  | UnpBinderListMetaVar (_,isopen,sl) :: l ->
+      let cl = pop bll in pr_binders (fun () -> aux sl) isopen cl ++ aux l
   | UnpTerminal s :: l -> str s ++ aux l
   | UnpBox (b,sub) :: l ->
       (* Keep order: side-effects *)
@@ -83,9 +85,9 @@ let print_hunks n pr (env,envlist) unp =
   | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in
   aux unp
 
-let pr_notation pr s env =
+let pr_notation pr pr_binders s env =
   let unpl, level = find_notation_printing_rule s in
-  print_hunks level pr env unpl, level
+  print_hunks level pr pr_binders env unpl, level
 
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
@@ -189,7 +191,8 @@ let rec pr_patt sep inh p =
       hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
   | CPatNotation (_,"( _ )",([p],[])) ->
       pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
-  | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
+  | CPatNotation (_,s,(l,ll)) ->
+      pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[])
   | CPatPrim (_,p) -> pr_prim_token p, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
@@ -252,18 +255,22 @@ let pr_binder_among_many pr_c = function
       hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c)
 
-let pr_undelimited_binders pr_c =
-  prlist_with_sep spc (pr_binder_among_many pr_c)
+let pr_undelimited_binders sep pr_c =
+  prlist_with_sep sep (pr_binder_among_many pr_c)
 
-let pr_delimited_binders kw pr_c bl =
+let pr_delimited_binders kw sep pr_c bl =
   let n = begin_of_binders bl in
   match bl with
   | [LocalRawAssum (nal,k,t)] ->
       pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
   | LocalRawAssum _ :: _ as bdl ->
-      pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl
+      pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
   | _ -> assert false
 
+let pr_binders_gen pr_c sep is_open =
+  if is_open then pr_delimited_binders mt sep pr_c
+  else pr_undelimited_binders sep pr_c
+
 let rec extract_prod_binders = function
 (*  | CLetIn (loc,na,b,c) as x ->
       let bl,c = extract_prod_binders c in
@@ -318,7 +325,7 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   let pr_body =
     if dangling_with_for then pr_dangling else pr in
   pr_id id ++ str" " ++
-  hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++
+  hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
@@ -438,14 +445,14 @@ let pr pr sep inherited a =
   | CProdN _ ->
       let (bl,a) = extract_prod_binders a in
       hov 0 (
-	hov 2 (pr_delimited_binders pr_forall
+	hov 2 (pr_delimited_binders pr_forall spc
                  (pr mt ltop) bl) ++
         str "," ++ pr spc ltop a),
       lprod
   | CLambdaN _ ->
       let (bl,a) = extract_lam_binders a in
       hov 0 (
-        hov 2 (pr_delimited_binders pr_fun
+        hov 2 (pr_delimited_binders pr_fun spc
                 (pr mt ltop) bl) ++
 	  Lazy.force pr_fun_sep ++ pr spc ltop a),
       llambda
@@ -545,9 +552,10 @@ let pr pr sep inherited a =
   | CCast (_,a,CastCoerce) ->
       hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
       lcast
-  | CNotation (_,"( _ )",([t],[])) ->
+  | CNotation (_,"( _ )",([t],[],[])) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
-  | CNotation (_,s,env) -> pr_notation (pr mt) s env
+  | CNotation (_,s,env) ->
+      pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env
   | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
   | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
@@ -619,7 +627,7 @@ let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
 
 let pr_cases_pattern_expr = pr_patt ltop
 
-let pr_binders = pr_undelimited_binders (pr ltop)
+let pr_binders = pr_undelimited_binders spc (pr ltop)
 
 let pr_with_occurrences pr occs =
   match occs with
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index dacc2b9b2..503fd734b 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -112,7 +112,9 @@ let pr_set_entry_type = function
   | ETConstr _ -> str"constr"
   | ETOther (_,e) -> str e
   | ETBigint -> str "bigint"
-  | ETConstrList _ -> failwith "Internal entry type"
+  | ETBinder true -> str "binder"
+  | ETBinder false -> str "closed binder"
+  | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
 
 let strip_meta id =
   let s = string_of_id id in
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index d78486a0b..20943f143 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -146,11 +146,10 @@ let rec mlexpr_of_constr = function
   | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >>
   | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)"
-  | Topconstr.CNotation(_,ntn,subst) ->
+  | Topconstr.CNotation(_,ntn,(subst,substl,[])) ->
       <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$
-              $mlexpr_of_pair
-                (mlexpr_of_list mlexpr_of_constr)
-                (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >>
+              ($mlexpr_of_list mlexpr_of_constr subst$,
+               $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >>
   | Topconstr.CPatVar (loc,n) ->
       <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
   | _ -> failwith "mlexpr_of_constr: TODO"