Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers

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

7 files changed, 206 insertions, 98 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 2858ada3a..1e33ea049 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -23,6 +23,10 @@ open Pretype_errors
 (*Takes a list of variables which must not be globalized*)
 let from_list l = List.fold_right Idset.add l Idset.empty
 
+let rec adjust_implicits n = function
+  | p::l -> if p<=n then adjust_implicits n l else (p-n)::adjust_implicits n l
+  | [] -> []
+
 (* when an head ident is not a constructor in pattern *)
 let mssg_hd_is_not_constructor s =
   [< 'sTR ("The symbol "^s^" should be a constructor") >]
@@ -178,17 +182,26 @@ let ast_to_global loc c =
   match c with
     | ("CONST", [sp]) ->
 	let ref = ConstRef (ast_to_sp sp) in
-	RRef (loc, ref), implicits_of_global ref
+	let hyps = implicit_section_args ref in
+	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
+	let imps = implicits_of_global ref in
+	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
     | ("MUTIND", [sp;Num(_,tyi)]) -> 
 	let ref = IndRef (ast_to_sp sp, tyi) in
-	RRef (loc, ref), implicits_of_global ref
+	let hyps = implicit_section_args ref in
+	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
+	let imps = implicits_of_global ref in
+	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
     | ("MUTCONSTRUCT", [sp;Num(_,ti);Num(_,n)]) ->
 	let ref = ConstructRef ((ast_to_sp sp,ti),n) in
-	RRef (loc, ref), implicits_of_global ref
+	let hyps = implicit_section_args ref in
+	let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
+	let imps = implicits_of_global ref in
+	RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
     | ("EVAR", [(Num (_,ev))]) ->
-	REvar (loc, ev), []
+	REvar (loc, ev), [], []
     | ("SYNCONST", [sp]) ->
-	Syntax_def.search_syntactic_definition (ast_to_sp sp), []
+	Syntax_def.search_syntactic_definition (ast_to_sp sp), [], []
     | _ -> anomaly_loc (loc,"ast_to_global",
 			[< 'sTR "Bad ast for this global a reference">])
 
@@ -208,7 +221,7 @@ let ref_from_constr c = match kind_of_term c with
 
 let ast_to_var (env,impls) (vars1,vars2) loc s =
   let id = id_of_string s in
-  let imp = 
+  let imps =
     if Idset.mem id env or List.mem s vars1
     then
       try List.assoc id impls
@@ -216,9 +229,11 @@ let ast_to_var (env,impls) (vars1,vars2) loc s =
     else
       let _ = lookup_id id vars2 in
       (* Car Fixpoint met les fns définies tmporairement comme vars de sect *)
-      try implicits_of_global (Nametab.locate (make_qualid [] s))
+      try
+	let ref = Nametab.locate (make_qualid [] s) in
+	implicits_of_global ref
       with _ -> []
-  in RVar (loc, id), imp
+  in RVar (loc, id), [], imps
 
 (********************************************************************)
 (* This is generic code to deal with globalization                  *)
@@ -267,12 +282,15 @@ let rawconstr_of_qualid env vars loc qid =
   (* Is it a global reference? *)
   try
     let ref = Nametab.locate qid in
-    RRef (loc, ref), implicits_of_global ref
+    let hyps = implicit_section_args ref in
+    let section_args = List.map (fun id -> RRef (loc, VarRef id)) hyps in
+    let imps = implicits_of_global ref in
+    RRef (loc, ref), section_args, adjust_implicits (List.length hyps) imps
   with Not_found ->
   (* Is it a reference to a syntactic definition? *)
   try
     let sp = Syntax_def.locate_syntactic_definition qid in
-    set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp), []
+    set_loc_of_rawconstr loc (Syntax_def.search_syntactic_definition sp),[],[]
   with Not_found ->
     error_global_not_found_loc loc qid
 
@@ -362,10 +380,12 @@ let check_capture loc s ty = function
 let ast_to_rawconstr sigma env allow_soapp lvar =
   let rec dbrec (ids,impls as env) = function
     | Nvar(loc,s) ->
-	fst (rawconstr_of_var env lvar loc s)
+	let f, hyps, _ = rawconstr_of_var env lvar loc s in
+	if hyps = [] then f else RApp (loc, f, hyps)
 
     | Node(loc,"QUALID", l) ->
-	fst (rawconstr_of_qualid env lvar loc (interp_qualid l))
+	let f, hyps, _ = rawconstr_of_qualid env lvar loc (interp_qualid l) in
+	if hyps = [] then f else RApp (loc, f, hyps)
   
     | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
 	let (lf,ln,lA,lt) = ast_to_fix ldecl in
@@ -396,23 +416,21 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	let na,ids' = match ona with
 	  | Some s -> let id = id_of_string s in Name id, Idset.add id ids
 	  | _ -> Anonymous, ids in
-	let kind = match k with
-	  | "PROD" -> BProd
-	  | "LAMBDA" -> BLambda
-	  | "LETIN" -> BLetIn
-	  | _ -> assert false in
-	RBinder(loc, kind, na, dbrec env c1, dbrec (ids',impls) c2)
-
-    | Node(_,"PRODLIST", [c1;(Slam _ as c2)]) -> 
-	iterated_binder BProd 0 c1 env c2
-    | Node(_,"LAMBDALIST", [c1;(Slam _ as c2)]) -> 
-	iterated_binder BLambda 0 c1 env c2
+	let c1' = dbrec env c1 and c2' = dbrec (ids',impls) c2 in
+	(match k with
+	   | "PROD" -> RProd (loc, na, c1', c2')
+	   | "LAMBDA" -> RLambda (loc, na, c1', c2')
+	   | "LETIN" -> RLetIn (loc, na, c1', c2')
+	   | _ -> assert false)
+
+    | Node(_,("PRODLIST"|"LAMBDALIST" as s), [c1;(Slam _ as c2)]) -> 
+	iterated_binder s 0 c1 env c2
 
     | Node(loc,"APPLISTEXPL", f::args) ->
 	RApp (loc,dbrec env f,ast_to_args env args)
 
     | Node(loc,"APPLIST", f::args) ->
-	let (c, impargs) =
+	let (c, hyps, impargs) =
 	  match f with
 	    | Node(locs,"QUALID",p) ->
 		rawconstr_of_qualid env lvar locs (interp_qualid p)
@@ -420,9 +438,9 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 		   ("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),
 		   l) ->
 		ast_to_global loc (key,l)
-	    | _ -> (dbrec env f, [])
+	    | _ -> (dbrec env f, [], [])
         in
-	  RApp (loc, c, ast_to_impargs env impargs args)
+	  RApp (loc, c, hyps @ (ast_to_impargs env impargs args))
 
     | Node(loc,"CASES", p:: Node(_,"TOMATCH",tms):: eqns) ->
 	let po = match p with 
@@ -452,7 +470,8 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	  
     (* This case mainly parses things build in a quotation *)
     | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
-	fst (ast_to_global loc (key,l))
+	let f, hyps, _ = ast_to_global loc (key,l) in
+	if hyps = [] then f else RApp (loc, f, hyps)	
 
     | Node(loc,"CAST", [c1;c2]) ->	   
 	RCast (loc,dbrec env c1,dbrec env c2)
@@ -495,8 +514,11 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	      let id = id_of_string s in Name id, Idset.add id ids
 	  | _ -> Anonymous, ids
 	in
-	RBinder(loc, oper, na, dbrec env ty,
-		(iterated_binder oper (n+1) ty (ids',impls) body))
+	let r = iterated_binder oper (n+1) ty (ids',impls) body in
+	(match oper with
+	   | "PRODLIST" -> RProd(loc, na, dbrec env ty, r)
+	   | "LAMBDALIST" -> RLambda(loc, na, dbrec env ty, r)
+	   | _ -> assert false)
     | body -> dbrec env body
 
   and ast_to_impargs env l args =
@@ -721,8 +743,14 @@ let rec pat_of_raw metas vars lvar = function
   | RApp (_,c,cl) -> 
       PApp (pat_of_raw metas vars lvar c,
 	    Array.of_list (List.map (pat_of_raw metas vars lvar) cl))
-  | RBinder (_,bk,na,c1,c2) ->
-      PBinder (bk, na, pat_of_raw metas vars lvar c1,
+  | RLambda (_,na,c1,c2) ->
+      PLambda (na, pat_of_raw metas vars lvar c1,
+	       pat_of_raw metas (na::vars) lvar c2)
+  | RProd (_,na,c1,c2) ->
+      PProd (na, pat_of_raw metas vars lvar c1,
+	       pat_of_raw metas (na::vars) lvar c2)
+  | RLetIn (_,na,c1,c2) ->
+      PLetIn (na, pat_of_raw metas vars lvar c1,
 	       pat_of_raw metas (na::vars) lvar c2)
   | RSort (_,s) ->
       PSort s
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index cddff7318..613b3c124 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -30,7 +30,7 @@ val interp_casted_openconstr    :
    declared in the rel_context of [env] *)
 val interp_type_with_implicits : 
   'a evar_map -> env -> 
-    impl_map:(identifier * int list) list -> Coqast.t -> types
+   (identifier * Impargs.implicits_list) list -> Coqast.t -> types
 
 val judgment_of_rawconstr : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
 val type_judgment_of_rawconstr :
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index a99046686..a4c9d9082 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -10,7 +10,7 @@ open Util
 open Names
 open Coqast
 open Ast
-open Stdlib
+open Coqlib
 open Termast
 
 exception Non_closed_number
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 2577ef9be..214317838 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -81,8 +81,85 @@ let implicit_args_msg sp mipv =
           >])
        mipv >]
 
-let print_mutual sp mib = 
-  let pk = kind_of_path sp in
+let print_params env params =
+  if List.length params = 0 then 
+    [<>] 
+  else
+    [< 'sTR "["; pr_rel_context env params; 'sTR "]"; 'bRK(1,2) >]
+
+let print_constructors envpar names types =
+  let pc =
+    [< prvect_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
+         (fun (id,c) -> [< pr_id id; 'sTR " : "; prterm_env envpar c >])
+	 (array_map2 (fun n t -> (n,t)) names types) >]
+  in hV 0 [< 'sTR "  "; pc >] 
+
+let build_inductive sp tyi =
+  let ctxt = context_of_global_reference (IndRef (sp,tyi)) in
+  let ctxt = Array.of_list (instance_from_section_context ctxt) in
+  let mis = Global.lookup_mind_specif ((sp,tyi),ctxt) in
+  let params = mis_params_ctxt mis in
+  let args = extended_rel_list 0 params in
+  let indf = make_ind_family (mis,args) in
+  let arity = get_arity_type indf in
+  let cstrtypes = get_constructors_types indf in
+  let cstrnames = mis_consnames mis in
+  (IndRef (sp,tyi), params, arity, cstrnames, cstrtypes)
+
+let print_one_inductive sp tyi =
+  let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
+  let env = Global.env () in
+  let envpar = push_rels params env in
+  (hOV 0
+     [< (hOV 0
+	   [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); print_params env params;
+	      'sTR ": "; prterm_env envpar arity; 'sTR " :=" >]);
+	'bRK(1,2); print_constructors envpar cstrnames cstrtypes >]) 
+
+let print_mutual sp =
+  let mipv = (Global.lookup_mind sp).mind_packets in
+  if Array.length mipv = 1 then
+    let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp 0 in
+    let sfinite =
+      if mipv.(0).mind_finite then "Inductive " else "CoInductive " in
+    let env = Global.env () in
+    let envpar = push_rels params env in
+    (hOV 0 [< 
+       'sTR sfinite ; 
+      pr_global (IndRef (sp,0)); 'bRK(1,2);
+       print_params env params; 'bRK(1,5);
+       'sTR": "; prterm_env envpar arity; 'sTR" :=";
+       'bRK(0,4); print_constructors envpar cstrnames cstrtypes; 'fNL;
+       implicit_args_msg sp mipv  >] )
+  (* Mutual [co]inductive definitions *)
+  else
+    let _,(mipli,miplc) =
+      Array.fold_right
+        (fun mi (n,(li,lc)) ->
+           if mi.mind_finite then (n+1,(n::li,lc)) else (n+1,(li,n::lc)))
+        mipv (0,([],[])) 
+    in 
+    let strind =
+      if mipli = [] then [<>] 
+      else [< 'sTR "Inductive"; 'bRK(1,4);
+              (prlist_with_sep
+                 (fun () -> [< 'fNL; 'sTR"  with"; 'bRK(1,4) >])
+                 (print_one_inductive sp) mipli); 'fNL >]
+    and strcoind =
+      if miplc = [] then [<>] 
+      else [< 'sTR "CoInductive"; 'bRK(1,4);
+              (prlist_with_sep
+                 (fun () -> [<'fNL; 'sTR "  with"; 'bRK(1,4) >]) 
+                 (print_one_inductive sp) miplc); 'fNL >] 
+    in
+    (hV 0 [< 'sTR"Mutual " ; 
+             if mipv.(0).mind_finite then 
+	       [< strind; strcoind >] 
+             else 
+	       [<strcoind; strind>];
+             implicit_args_msg sp mipv >])
+
+(*
   let env = Global.env () in
   let evd = Evd.empty in
   let {mind_packets=mipv} = mib in 
@@ -113,7 +190,10 @@ let print_mutual sp mib =
       [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >] in
   let print_oneind tyi =
     let mis =
-      build_mis ((sp,tyi),Array.of_list (instance_from_named_context mib.mind_hyps)) mib in
+      build_mis
+	((sp,tyi),
+	 Array.of_list (instance_from_section_context mib.mind_hyps))
+	mib in
     let (_,arity) = decomp_n_prod env evd nparams
 		      (body_of_type (mis_user_arity mis)) in
       (hOV 0
@@ -123,7 +203,9 @@ let print_mutual sp mib =
             'bRK(1,2); print_constructors mis >]) 
   in 
   let mis0 =
-    build_mis ((sp,0),Array.of_list (instance_from_named_context mib.mind_hyps)) mib in
+    build_mis
+      ((sp,0),Array.of_list (instance_from_section_context mib.mind_hyps))
+      mib in
   (* Case one [co]inductive *)
   if Array.length mipv = 1 then
     let (_,arity) = decomp_n_prod env evd nparams
@@ -165,7 +247,7 @@ let print_mutual sp mib =
              else 
 	       [<strcoind; strind>];
              implicit_args_msg sp mipv >])
-
+*)
 let print_section_variable sp =
   let (d,_,_) = get_variable sp in
   let l = implicits_of_var sp in
@@ -202,9 +284,8 @@ let print_constant with_values sep sp =
 	     print_basename sp ; 'fNL>]
 
 let print_inductive sp =
-  let mib = Global.lookup_mind sp in
   if kind_of_path sp = CCI then
-    [< print_mutual sp mib; 'fNL >]
+    [< print_mutual sp; 'fNL >]
   else
     hOV 0 [< 'sTR"Fw inductive definition "; 
 	     print_basename sp; 'fNL >]
@@ -359,7 +440,7 @@ let print_opaque_name qid =
           else 
 	    anomaly "print_opaque_name"
       | IsMutInd ((sp,_),_) ->
-          print_mutual sp (Global.lookup_mind sp)
+          print_mutual sp
       | IsMutConstruct cstr -> 
 	  let ty = Typeops.type_of_constructor env sigma cstr in
 	  print_typed_value (x, ty)
@@ -393,8 +474,7 @@ let print_local_context () =
                   print_basename sp ;'sTR" = ";
                   print_typed_body (val_0,typ) >]
            | "INDUCTIVE" -> 
-               let mib = Global.lookup_mind sp in 
-               [< print_last_const rest;print_mutual sp mib; 'fNL >]
+               [< print_last_const rest;print_mutual sp; 'fNL >]
            | "VARIABLE" ->  [< >]
            | _          ->  print_last_const rest)
     | _ -> [< >]
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index 0a1ed41f3..c224bc20d 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -27,8 +27,7 @@ val print_val : env -> unsafe_judgment -> std_ppcmds
 val print_type : env -> unsafe_judgment -> std_ppcmds
 val print_eval :
   'a reduction_function -> env -> unsafe_judgment -> std_ppcmds
-val print_mutual :
-  section_path -> Declarations.mutual_inductive_body -> std_ppcmds
+val print_mutual : section_path -> std_ppcmds
 val print_name : qualid -> std_ppcmds
 val print_opaque_name : qualid -> std_ppcmds
 val print_local_context : unit -> std_ppcmds
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 97a876133..d0535fbac 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -165,11 +165,11 @@ let pr_rel_decl env (na,c,typ) =
     | Some c ->
 	(* Force evaluation *) 
 	let pb = prterm_env env c in
-	[< 'sTR" :="; 'sPC; pb >] in
+	[< 'sTR" :="; 'sPC; pb; 'sPC >] in
   let ptyp = prtype_env env typ in
   match na with
-    | Anonymous -> [< 'sTR"<>" ; 'sPC; pbody; 'sTR" :"; 'sPC; ptyp >]
-    | Name id -> [< pr_id id ; 'sPC; pbody; 'sTR" :"; 'sPC; ptyp >]
+    | Anonymous -> [< 'sTR"<>" ; 'sPC; pbody; 'sTR":"; 'sPC; ptyp >]
+    | Name id -> [< pr_id id ; 'sPC; pbody; 'sTR":"; 'sPC; ptyp >]
 
 
 (* Prints out an "env" in a nice format.  We print out the
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 0a7a73966..b1a2d18d1 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -118,6 +118,12 @@ let ast_dependent na aty =
     | Name id -> occur_var_ast (string_of_id id) aty
     | Anonymous -> false
 
+let decompose_binder = function
+  | RProd(_,na,ty,c) -> Some (BProd,na,ty,c)
+  | RLambda(_,na,ty,c) -> Some (BLambda,na,ty,c)
+  | RLetIn(_,na,b,c) -> Some (BLetIn,na,b,c)
+  | _ -> None
+
 (* Implicit args indexes are in ascending order *)
 let explicitize =
   let rec exprec n lastimplargs impl = function
@@ -155,22 +161,6 @@ let ast_of_app impl f args =
     ope("APPLISTEXPL", f::args)
   else
     ope("APPLIST", f::(explicitize impl args))
-(*
-    let largs = List.length args in
-    let impl = List.rev (List.filter (fun i -> i <= largs) impl) in
-    let impl1,impl2 = div_implicits largs impl in
-    let al1 = Array.of_list args in
-    List.iter
-      (fun i -> al1.(i) <-
-         ope("EXPL", [str "EX"; num i; al1.(i)]))
-      impl2;
-    List.iter
-      (fun i -> al1.(i) <-
-         ope("EXPL",[num i; al1.(i)]))
-      impl1;
-    (* On laisse les implicites, à charge du PP de ne pas les imprimer *)
-    ope("APPLISTEXPL",f::(Array.to_list al1))
-*)
 
 let rec ast_of_raw = function
   | RRef (_,ref) -> ast_of_ref ref
@@ -194,25 +184,28 @@ let rec ast_of_raw = function
 	       with Not_found -> [] in
 	     ast_of_app imp astf astargs
 	 | _       -> ast_of_app [] astf astargs)
-  | RBinder (_,BProd,Anonymous,t,c) ->
+
+  | RProd (_,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
       ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])
-  | RBinder (_,BLetIn,na,t,c) ->
+
+  | RLetIn (_,na,t,c) ->
       ope("LETIN",[ast_of_raw t; slam(stringopt_of_name na,ast_of_raw c)])
-  | RBinder (_,bk,na,t,c) ->
-      let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in
-      let tag = match bk with
-	  (* LAMBDA et LAMBDALIST se comportent pareil ... Non ! *)
-	  (* Pour compatibilité des theories, il faut LAMBDALIST partout *)
-	| BLambda -> (* if n=1 then "LAMBDA" else *) "LAMBDALIST"
-	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
-	  (* non dépendant, pour isoler l'implication; peut-être un *)
-	  (* constructeur ARROW serait-il plus justifié ? *) 
-	| BProd -> if n=1 then "PROD" else "PRODLIST" 
-	| BLetIn -> if n=1 then "LETIN" else "LETINLIST" 
-      in
+
+  | RProd (_,na,t,c) ->
+      let (n,a) = factorize_binder 1 BProd na (ast_of_raw t) c in
+      (* PROD et PRODLIST doivent être distingués à cause du cas *)
+      (* non dépendant, pour isoler l'implication; peut-être un *)
+      (* constructeur ARROW serait-il plus justifié ? *) 
+      let tag = if n=1 then "PROD" else "PRODLIST" in
       ope(tag,[ast_of_raw t;a])
 
+  | RLambda (_,na,t,c) ->
+      let (n,a) = factorize_binder 1 BLambda na (ast_of_raw t) c in
+      (* LAMBDA et LAMBDALIST se comportent pareil ... Non ! *)
+      (* Pour compatibilité des theories, il faut LAMBDALIST partout *)
+      ope("LAMBDALIST",[ast_of_raw t;a])
+
   | RCases (_,printinfo,typopt,tml,eqns) ->
       let pred = ast_of_rawopt typopt in
       let tag = match printinfo with
@@ -235,13 +228,13 @@ let rec ast_of_raw = function
 	 | RFix (nv,n) ->
              let rec split_lambda binds = function
 	       | (0, t) -> (binds,ast_of_raw t)
-	       | (n, RBinder(_,BLambda,na,t,b)) ->
+	       | (n, RLambda (_,na,t,b)) ->
 		   let bind = ope("BINDER",[ast_of_raw t;ast_of_name na]) in
 		   split_lambda (bind::binds) (n-1,b)
 	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
 	     let rec split_product = function
 	       | (0, t) -> ast_of_raw t
-	       | (n, RBinder(_,BProd,na,t,b)) -> split_product (n-1,b)
+	       | (n, RProd (_,na,t,b)) -> split_product (n-1,b)
 	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
 	     let listdecl = 
 	       Array.mapi
@@ -279,8 +272,8 @@ and ast_of_rawopt = function
   | Some p -> ast_of_raw p
 
 and factorize_binder n oper na aty c =
-  let (p,body) = match c with
-    | RBinder(_,oper',na',ty',c')
+  let (p,body) = match decompose_binder c with
+    | Some (oper',na',ty',c')
 	when (oper = oper') & (aty = ast_of_raw ty')
 	  & not (ast_dependent na aty) (* To avoid na in ty' escapes scope *)
 	  & not (na' = Anonymous & oper = BProd)
@@ -326,6 +319,12 @@ let ast_of_inductive env (ind_sp,ids) =
     ope("INSTANCE",a::(array_map_to_list (ast_of_constr false env) ids))
   else a
 
+let decompose_binder_pattern = function
+  | PProd(na,ty,c) -> Some (BProd,na,ty,c)
+  | PLambda(na,ty,c) -> Some (BLambda,na,ty,c)
+  | PLetIn(na,b,c) -> Some (BLetIn,na,b,c)
+  | _ -> None
+
 let rec ast_of_pattern env = function
   | PRef ref -> ast_of_ref ref
 
@@ -356,25 +355,27 @@ let rec ast_of_pattern env = function
       ope("SOAPP",(ope ("META",[num n])):: 
 		  (List.map (ast_of_pattern env) args))
 
-  | PBinder (BLetIn,na,b,c) ->
+  | PLetIn (na,b,c) ->
       let c' = ast_of_pattern (add_name na env) c in
       ope("LETIN",[ast_of_pattern env b;slam(stringopt_of_name na,c')])
 		
-  | PBinder (BProd,Anonymous,t,c) ->
+  | PProd (Anonymous,t,c) ->
       ope("PROD",[ast_of_pattern env t; slam(None,ast_of_pattern env c)])
-  | PBinder (bk,na,t,c) ->
+  | PProd (na,t,c) ->
       let env' = add_name na env in
-      let (n,a) = factorize_binder_pattern
-		    env' 1 bk na (ast_of_pattern env t) c in
-      let tag = match bk with
-	  (* LAMBDA et LAMBDALIST se comportent pareil *)
-	| BLambda -> if n=1 then "LAMBDA" else "LAMBDALIST"
-	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
-	  (* non dépendant, pour isoler l'implication; peut-être un *)
-	  (* constructeur ARROW serait-il plus justifié ? *) 
-	| BProd -> if n=1 then "PROD" else "PRODLIST" 
-	| BLetIn -> anomaly "Should be captured before"
-      in
+      let (n,a) =
+	factorize_binder_pattern env' 1 BProd na (ast_of_pattern env t) c in
+      (* PROD et PRODLIST doivent être distingués à cause du cas *)
+      (* non dépendant, pour isoler l'implication; peut-être un *)
+      (* constructeur ARROW serait-il plus justifié ? *) 
+      let tag = if n=1 then "PROD" else "PRODLIST" in
+      ope(tag,[ast_of_pattern env t;a])
+  | PLambda (na,t,c) ->
+      let env' = add_name na env in
+      let (n,a) =
+	factorize_binder_pattern env' 1 BLambda na (ast_of_pattern env t) c in
+      (* LAMBDA et LAMBDALIST se comportent pareil *)
+      let tag = if n=1 then "LAMBDA" else "LAMBDALIST" in
       ope(tag,[ast_of_pattern env t;a])
 
   | PCase (typopt,tm,bv) ->
@@ -399,8 +400,8 @@ and ast_of_patopt env = function
   | Some p -> ast_of_pattern env p
 
 and factorize_binder_pattern env n oper na aty c =
-  let (p,body) = match c with
-    | PBinder(oper',na',ty',c')
+  let (p,body) = match decompose_binder_pattern c with
+    | Some (oper',na',ty',c')
 	when (oper = oper') & (aty = ast_of_pattern env ty')
 	  & not (na' = Anonymous & oper = BProd)
 	  ->