A patch for printing "match" when constructors are defined with let-in

but the internal representation dropped let-in.

Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.

To do, there is still an extra @ in the constructor name that does not
need to be there.

17 files changed, 141 insertions, 90 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 1313208a3..f00c95705 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -53,7 +53,8 @@ type metavariable = int
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
   | RegularStyle (** infer printing form from number of constructor *)
 type case_printing =
-  { ind_nargs : int; (** length of the arity of the inductive type *)
+  { ind_tags : bool list; (* tell whether letin or lambda in the arity of the inductive type *)
+    cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *)
     style     : case_style }
 
 (** the integer is the number of real args, needed for reduction *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8e6485b7b..40e0901be 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -999,7 +999,7 @@ let rec glob_of_pat env sigma = function
   | PIf (c,b1,b2) ->
       GIf (loc, glob_of_pat env sigma c, (Anonymous,None),
            glob_of_pat env sigma b1, glob_of_pat env sigma b2)
-  | PCase ({cip_style=LetStyle; cip_ind_args=None},PMeta None,tm,[(0,n,b)]) ->
+  | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
       let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in
       GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env sigma tm,b)
   | PCase (info,p,tm,bl) ->
@@ -1012,7 +1012,7 @@ let rec glob_of_pat env sigma = function
       in
       let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
       in
-      let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with
+      let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with
 	| PMeta None, _, _ -> (Anonymous,None),None
 	| _, Some ind, Some nargs ->
 	  return_type_of_predicate ind nargs (glob_of_pat env sigma p)
diff --git a/intf/pattern.mli b/intf/pattern.mli
index 4fa5f418d..b04db3bfa 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -55,7 +55,7 @@ type extended_patvar_map = constr_under_binders Id.Map.t
 type case_info_pattern =
     { cip_style : case_style;
       cip_ind : inductive option;
-      cip_ind_args : int option; (** number of params and args *)
+      cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *)
       cip_extensible : bool (** does this match end with _ => _ ? *) }
 
 type constr_pattern =
@@ -73,7 +73,7 @@ type constr_pattern =
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
   | PCase of case_info_pattern * constr_pattern * constr_pattern *
-      (int * int * constr_pattern) list (** index of constructor, nb of args *)
+      (int * bool list * constr_pattern) list (** index of constructor, nb of args *)
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 912067629..f688cca45 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -38,7 +38,8 @@ type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_nargs : int; (* length of the arity of the inductive type *)
+  { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
+    cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *)
     style     : case_style }
 type case_info =
   { ci_ind        : inductive;
@@ -933,7 +934,8 @@ struct
   type u = inductive -> inductive
   let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
   let pp_info_equal info1 info2 =
-    Int.equal info1.ind_nargs info2.ind_nargs &&
+    List.equal (==) info1.ind_tags info2.ind_tags &&
+    Array.equal (List.equal (==)) info1.cstr_tags info2.cstr_tags &&
     info1.style == info2.style
   let equal ci ci' =
     ci.ci_ind == ci'.ci_ind &&
@@ -942,15 +944,18 @@ struct
     Array.equal Int.equal ci.ci_cstr_nargs ci'.ci_cstr_nargs && (* we use [Array.equal] on purpose *)
     pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
   open Hashset.Combine
+  let hash_bool b = if b then 0 else 1
+  let hash_bool_list = List.fold_left (fun n b -> combine n (hash_bool b))
   let hash_pp_info info =
-    let h = match info.style with
+    let h1 = match info.style with
     | LetStyle -> 0
     | IfStyle -> 1
     | LetPatternStyle -> 2
     | MatchStyle -> 3
-    | RegularStyle -> 4
-    in
-    combine info.ind_nargs h
+    | RegularStyle -> 4 in
+    let h2 = hash_bool_list 0 info.ind_tags in
+    let h3 = Array.fold_left hash_bool_list 0 info.cstr_tags in
+    combine3 h1 h2 h3
   let hash ci =
     let h1 = ind_hash ci.ci_ind in
     let h2 = Int.hash ci.ci_npar in
diff --git a/kernel/constr.mli b/kernel/constr.mli
index da7ac6a0d..1e23911dd 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -26,7 +26,8 @@ type metavariable = int
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle 
   | RegularStyle (** infer printing form from number of constructor *)
 type case_printing =
-  { ind_nargs : int; (** length of the arity of the inductive type *)
+  { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
+    cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *)
     style     : case_style }
 
 (** the integer is the number of real args, needed for reduction *)
diff --git a/kernel/context.ml b/kernel/context.ml
index 5256ee417..5cb964b9c 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -76,6 +76,13 @@ let rel_context_nhyps hyps =
     | (_,Some _,_)::hyps -> nhyps acc hyps in
   nhyps 0 hyps
 
+let rel_context_tags ctx =
+  let rec aux l = function
+  | [] -> l
+  | (_,Some _,_)::ctx -> aux (true::l) ctx
+  | (_,None _,_)::ctx -> aux (false::l) ctx
+  in aux [] ctx
+
 (*s Signatures of named hypotheses. Used for section variables and
     goal assumptions. *)
 
diff --git a/kernel/context.mli b/kernel/context.mli
index 1d732d273..b7eb7a76a 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -115,3 +115,5 @@ val lookup_rel : int -> rel_context -> rel_declaration
 val rel_context_length : rel_context -> int
 (** Size of the [rel_context] without LetIns *)
 val rel_context_nhyps : rel_context -> int
+(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
+val rel_context_tags : rel_context -> bool list
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 39455a7d2..45e0261d3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -666,7 +666,8 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
   let mp, dp, l = repr_mind kn in
   let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
   let ci = 
-    let print_info = { ind_nargs = 0; style = LetStyle } in
+    let print_info =
+      { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
       { ci_ind     = ind;
 	ci_npar    = nparamargs;
 	ci_cstr_ndecls = mind_consnrealdecls;
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 041751ecf..c8a4fa897 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1807,7 +1807,7 @@ let compile_constant env sigma prefix ~interactive con cb =
       let ci = { ci_ind = ind; ci_npar = mib.mind_nparams; 
 		 ci_cstr_nargs = [|0|];
 		 ci_cstr_ndecls = [||] (*FIXME*);
-		 ci_pp_info = { ind_nargs = 0; style = RegularStyle } } in
+		 ci_pp_info = { ind_tags = []; cstr_tags = [||] (*FIXME*); style = RegularStyle } } in
       let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci;
 		  asw_reloc = tbl; asw_finite = true } in
       let c_uid = fresh_lname Anonymous in
diff --git a/kernel/term.ml b/kernel/term.ml
index 734b7853f..3adfa5e37 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -40,7 +40,7 @@ type case_style = Constr.case_style =
   LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 
 type case_printing = Constr.case_printing =
-  { ind_nargs : int; style     : case_style }
+  { ind_tags : bool list; cstr_tags : bool list array; style : case_style }
 
 type case_info = Constr.case_info =
   { ci_ind        : inductive;
diff --git a/kernel/term.mli b/kernel/term.mli
index 50cd433e9..c5e85b1e5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -47,7 +47,7 @@ type case_style = Constr.case_style =
   LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 
 type case_printing = Constr.case_printing =
-  { ind_nargs : int; style     : case_style }
+  { ind_tags : bool list; cstr_tags : bool list array; style : case_style }
 
 type case_info = Constr.case_info =
   { ci_ind        : inductive;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e9a1174b4..2d7c7b146 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -172,7 +172,7 @@ let computable p k =
        works for normal eta-expanded term. For non eta-expanded or
        non-normal terms, it may affirm the pred is synthetisable
        because of an undetected ultimate dependent variable in the second
-       clause, or else, it may affirms the pred non synthetisable
+       clause, or else, it may affirm the pred non synthetisable
        because of a non normal term in the fourth clause.
        A solution could be to store, in the MutCase, the eta-expanded
        normal form of pred to decide if it depends on its variables
@@ -239,26 +239,29 @@ let update_name na ((_,(e,_)),c) =
   | _ ->
       na
 
-let rec decomp_branch ndecls nargs nal b (avoid,env as e) c =
+let rec decomp_branch tags nal b (avoid,env as e) c =
   let flag = if b then RenamingForGoal else RenamingForCasesPattern (fst env,c) in
-  if Int.equal ndecls 0 then (List.rev nal,(e,c))
-  else
-    let na,c,f,nargs',body,t =
-      match kind_of_term (strip_outer_cast c) with
-	| Lambda (na,t,c) -> na,c,compute_displayed_let_name_in,nargs-1,None,Some t
-	| LetIn (na,b,t,c) when ndecls>nargs ->
-            na,c,compute_displayed_name_in,nargs,Some b,Some t
-	| _ ->
+  match tags with
+  | [] -> (List.rev nal,(e,c))
+  | b::tags ->
+      let na,c,f,body,t =
+        match kind_of_term (strip_outer_cast c), b with
+	| Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t
+	| LetIn (na,b,t,c),true ->
+            na,c,compute_displayed_name_in,Some b,Some t
+	| _, false ->
 	  Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])),
-	    compute_displayed_name_in,nargs-1,None,None
+	    compute_displayed_name_in,None,None
+	| _, true ->
+	  Anonymous,lift 1 c,compute_displayed_name_in,None,None
     in
     let na',avoid' = f flag avoid na c in
-    decomp_branch (ndecls-1) nargs' (na'::nal) b 
+    decomp_branch tags (na'::nal) b
       (avoid', add_name_opt na' body t env) c
 
 let rec build_tree na isgoal e ci cl =
   let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
-  let cnl = ci.ci_cstr_ndecls in
+  let cnl = ci.ci_pp_info.cstr_tags in
   let cna = ci.ci_cstr_nargs in
   List.flatten
     (List.init (Array.length cl)
@@ -271,7 +274,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
     | Case (ci,p,c,cl) when
         eq_constr c (mkRel (List.index Name.equal na (fst (snd e))))
 	&& (* don't contract if p dependent *)
-	computable p (ci.ci_pp_info.ind_nargs) ->
+	computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
 	let clauses = build_tree na isgoal e ci cl in
 	List.flatten
           (List.map (fun (pat,rhs) ->
@@ -284,7 +287,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
 	List.map (fun (hd,rest) -> pat::hd,rest) mat
 
 and contract_branch isgoal e (cdn,can,mkpat,b) =
-  let nal,rhs = decomp_branch cdn can [] isgoal e b in
+  let nal,rhs = decomp_branch cdn [] isgoal e b in
   let mat = align_tree nal isgoal rhs in
   List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat
 
@@ -292,27 +295,32 @@ and contract_branch isgoal e (cdn,can,mkpat,b) =
 (* Transform internal representation of pattern-matching into list of *)
 (* clauses                                                            *)
 
-let is_nondep_branch c n =
+let is_nondep_branch c l =
   try
-    let sign,ccl = decompose_lam_n_assum n c in
+    (* FIXME: do better using tags from l *)
+    let sign,ccl = decompose_lam_n_assum (List.length l) c in
     noccur_between 1 (rel_context_length sign) ccl
   with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
 
-let extract_nondep_branches test c b n =
-  let rec strip n r = if Int.equal n 0 then r else
-    match r with
-      | GLambda (_,_,_,_,t) -> strip (n-1) t
-      | GLetIn (_,_,_,t) -> strip (n-1) t
-      | _ -> assert false in
-  if test c n then Some (strip n b) else None
-
-let it_destRLambda_or_LetIn_names n c =
-  let rec aux n nal c =
-    if Int.equal n 0 then (List.rev nal,c) else match c with
-      | GLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c
-      | GLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
-      | _ ->
+let extract_nondep_branches test c b l =
+  let rec strip l r =
+    match r,l with
+      | r, [] -> r
+      | GLambda (_,_,_,_,t), false::l -> strip l t
+      | GLetIn (_,_,_,t), true::l -> strip l t
+      (* FIXME: do we need adjustment? *)
+      | _,_ -> assert false in
+  if test c l then Some (strip l b) else None
+
+let it_destRLambda_or_LetIn_names l c =
+  let rec aux l nal c =
+    match c, l with
+      | _, [] -> (List.rev nal,c)
+      | GLambda (_,na,_,_,c), false::l -> aux l (na::nal) c
+      | GLetIn (_,na,_,c), true::l -> aux l (na::nal) c
+      | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c
+      | _, false::l ->
           (* eta-expansion *)
 	  let next l =
 	    let x = next_ident_away default_dependent_ident l in
@@ -322,14 +330,14 @@ let it_destRLambda_or_LetIn_names n c =
 	  in
 	  let x = next (free_glob_vars c) in
 	  let a = GVar (dl,x) in
-	  aux (n-1) (Name x :: nal)
+	  aux l (Name x :: nal)
             (match c with
               | GApp (loc,p,l) -> GApp (loc,p,l@[a])
               | _ -> (GApp (dl,c,[a])))
-  in aux n [] c
+  in aux l [] c
 
 let detype_case computable detype detype_eqns testdep avoid data p c bl =
-  let (indsp,st,consnargsl,k) = data in
+  let (indsp,st,constagsl,k) = data in
   let synth_type = synthetize_type () in
   let tomatch = detype c in
   let alias, aliastyp, pred=
@@ -367,20 +375,20 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
   match tag, aliastyp with
   | LetStyle, None ->
       let bl' = Array.map detype bl in
-      let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
+      let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in
       GLetTuple (dl,nal,(alias,pred),tomatch,d)
   | IfStyle, None ->
       let bl' = Array.map detype bl in
       let nondepbrs =
-	Array.map3 (extract_nondep_branches testdep) bl bl' consnargsl in
+	Array.map3 (extract_nondep_branches testdep) bl bl' constagsl in
       if Array.for_all ((!=) None) nondepbrs then
 	GIf (dl,tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
-	let eqnl = detype_eqns constructs consnargsl bl in
+	let eqnl = detype_eqns constructs constagsl bl in
 	GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
-      let eqnl = detype_eqns constructs consnargsl bl in
+      let eqnl = detype_eqns constructs constagsl bl in
       GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
@@ -513,12 +521,12 @@ let rec detype flags avoid env sigma t =
     | Construct (cstr_sp,u) ->
 	GRef (dl, ConstructRef cstr_sp, detype_instance u)
     | Case (ci,p,c,bl) ->
-	let comp = computable p (ci.ci_pp_info.ind_nargs) in
+	let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in
 	detype_case comp (detype flags avoid env sigma)
 	  (detype_eqns flags avoid env sigma ci comp)
 	  is_nondep_branch avoid
 	  (ci.ci_ind,ci.ci_pp_info.style,
-	   ci.ci_cstr_ndecls,ci.ci_pp_info.ind_nargs)
+	   ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
 	  (Some p) c bl
     | Fix (nvn,recdef) -> detype_fix flags avoid env sigma nvn recdef
     | CoFix (n,recdef) -> detype_cofix flags avoid env sigma n recdef
@@ -610,31 +618,35 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
       let na,avoid' = compute_displayed_name_in flag avoid x b in
       PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na
   in
-  let rec buildrec ids patlist avoid env n b =
-    if Int.equal n 0 then
-      (dl, Id.Set.elements ids,
-       [PatCstr(dl, constr, List.rev patlist,Anonymous)],
-       detype flags avoid env sigma b)
-    else
-      match kind_of_term b with
-	| Lambda (x,t,b) ->
+  let rec buildrec ids patlist avoid env l b =
+    match kind_of_term b, l with
+      | _, [] ->
+        (dl, Id.Set.elements ids,
+         [PatCstr(dl, constr, List.rev patlist,Anonymous)],
+         detype flags avoid env sigma b)
+      | Lambda (x,t,b), false::l ->
 	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in
-            buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
+            buildrec new_ids (pat::patlist) new_avoid new_env l b
 
-	| LetIn (x,b,t,b') ->
+      | LetIn (x,b,t,b'), true::l ->
 	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b' (Some b) t ids in
-            buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b'
+            buildrec new_ids (pat::patlist) new_avoid new_env l b'
+
+      | Cast (c,_,_), l ->    (* Oui, il y a parfois des cast *)
+	    buildrec ids patlist avoid env l c
 
-	| Cast (c,_,_) ->    (* Oui, il y a parfois des cast *)
-	    buildrec ids patlist avoid env n c
+      | _, true::l ->
+	    let pat = PatVar (dl,Anonymous) in
+            buildrec ids (pat::patlist) avoid env l b
 
-	| _ -> (* eta-expansion : n'arrivera plus lorsque tous les
-                  termes seront construits à partir de la syntaxe Cases *)
+      | _, false::l ->
+            (* eta-expansion : n'arrivera plus lorsque tous les
+               termes seront construits à partir de la syntaxe Cases *)
             (* nommage de la nouvelle variable *)
 	    let new_b = applist (lift 1 b, [mkRel 1]) in
             let pat,new_avoid,new_env,new_ids =
 	      make_pat Anonymous avoid env new_b None mkProp ids in
-	    buildrec new_ids (pat::patlist) new_avoid new_env (n-1) new_b
+	    buildrec new_ids (pat::patlist) new_avoid new_env l new_b
 
   in
   buildrec Id.Set.empty [] avoid env construct_nargs branch
@@ -800,6 +812,6 @@ let simple_cases_matrix_of_branches ind brs =
       (Loc.ghost,ids,[p],c))
     brs
 
-let return_type_of_predicate ind nrealargs_ctxt pred =
-  let nal,p = it_destRLambda_or_LetIn_names (nrealargs_ctxt+1) pred in
+let return_type_of_predicate ind nrealargs_tags pred =
+  let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in
   (List.hd nal, Some (Loc.ghost, ind, List.tl nal)), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index b2fc92557..8a8312990 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -34,10 +34,10 @@ val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob
 
 val detype_case :
   bool -> ('a -> glob_constr) ->
-  (constructor array -> int array -> 'a array ->
+  (constructor array -> bool list array -> 'a array ->
     (Loc.t * Id.t list * cases_pattern list * glob_constr) list) ->
-  ('a -> int -> bool) ->
-  Id.t list -> inductive * case_style * int array * int ->
+  ('a -> bool list -> bool) ->
+  Id.t list -> inductive * case_style * bool list array * bool list ->
     'a option -> 'a -> 'a array -> glob_constr
 
 val detype_sort : sorts -> glob_sort
@@ -55,11 +55,11 @@ val synthetize_type : unit -> bool
 
 (** Utilities to transform kernel cases to simple pattern-matching problem *)
 
-val it_destRLambda_or_LetIn_names : int -> glob_constr -> Name.t list * glob_constr
+val it_destRLambda_or_LetIn_names : bool list -> glob_constr -> Name.t list * glob_constr
 val simple_cases_matrix_of_branches :
-  inductive -> (int * int * glob_constr) list -> cases_clauses
+  inductive -> (int * bool list * glob_constr) list -> cases_clauses
 val return_type_of_predicate :
-  inductive -> int -> glob_constr -> predicate_pattern * glob_constr option
+  inductive -> bool list -> glob_constr -> predicate_pattern * glob_constr option
 
 val subst_genarg_hook :
   (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 91072dce8..70c670e3f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -273,7 +273,14 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let print_info = { ind_nargs = mip.mind_nrealdecls; style = style } in
+  let ind_tags =
+    rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in
+  let cstr_tags =
+    Array.map2 (fun c n ->
+      let d,_ = decompose_prod_assum c in
+      rel_context_tags (List.firstn n d))
+      mip.mind_nf_lc mip.mind_consnrealdecls in
+  let print_info = { ind_tags; cstr_tags; style } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
     ci_cstr_ndecls = mip.mind_consnrealdecls;
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 8c553f613..0576ec57b 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -26,7 +26,7 @@ open Environ
 let case_info_pattern_eq i1 i2 =
   i1.cip_style == i2.cip_style &&
   Option.equal eq_ind i1.cip_ind i2.cip_ind &&
-  Option.equal Int.equal i1.cip_ind_args i2.cip_ind_args &&
+  Option.equal (List.equal (==)) i1.cip_ind_tags i2.cip_ind_tags &&
   i1.cip_extensible == i2.cip_extensible
 
 let rec constr_pattern_eq p1 p2 = match p1, p2 with
@@ -63,7 +63,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 (** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
 
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
-  Int.equal i1 i2 && Int.equal j1 j2 && constr_pattern_eq p1 p2
+  Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2
 
 and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) =
   Int.equal i1 i2 &&
@@ -167,11 +167,11 @@ let pattern_of_constr env sigma t =
         let cip =
 	  { cip_style = ci.ci_pp_info.style;
 	    cip_ind = Some ci.ci_ind;
-	    cip_ind_args = Some (ci.ci_pp_info.ind_nargs);
+	    cip_ind_tags = Some ci.ci_pp_info.ind_tags;
 	    cip_extensible = false }
 	in
 	let branch_of_constr i c =
-	  (i, ci.ci_cstr_ndecls.(i), pattern_of_constr env c)
+	  (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c)
 	in
 	PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
 	       Array.to_list (Array.mapi branch_of_constr br))
@@ -360,17 +360,18 @@ let rec pat_of_raw metas vars = function
       let cip =
 	{ cip_style = LetStyle;
 	  cip_ind = None;
-	  cip_ind_args = None;
+	  cip_ind_tags = None;
 	  cip_extensible = false }
       in
+      let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in
       PCase (cip, PMeta None, pat_of_raw metas vars b,
-             [0,1,pat_of_raw metas vars c])
+             [0,tags,pat_of_raw metas vars c])
   | GCases (loc,sty,p,[c,(na,indnames)],brs) ->
       let get_ind = function
 	| (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
 	| _ -> None
       in
-      let ind_nargs,ind = match indnames with
+      let ind_tags,ind = match indnames with
 	| Some (_,ind,nal) -> Some (List.length nal), Some ind
 	| None -> None, get_ind brs
       in
@@ -385,7 +386,7 @@ let rec pat_of_raw metas vars = function
       let info =
 	{ cip_style = sty;
 	  cip_ind = ind;
-	  cip_ind_args = ind_nargs;
+	  cip_ind_tags = None;
 	  cip_extensible = ext }
       in
       (* Nota : when we have a non-trivial predicate,
@@ -416,7 +417,8 @@ and pats_of_glob_branches loc metas vars ind brs =
       let vars' = List.rev lna @ vars in
       let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
       let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
-      ext, ((j-1, List.length lv, pat) :: pats)
+      let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
+      ext, ((j-1, tags, pat) :: pats)
     | (loc,_,_,_) :: _ -> err loc (Pp.str "Non supported pattern.")
   in
   get_pat Int.Set.empty brs
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index c768f09ce..0ebc251bc 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -8,6 +8,14 @@ fix F (t : t) : P t :=
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
 t_rect is not universe polymorphic
+     = fun d : A => match d with
+                    | @C _ _ b => b
+                    end
+     : A -> 0 = 0
+     = fun d : A => match d with
+                    | @C _ _ b => b
+                    end
+     : A -> 0 = 0
 proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
 match Nat.eq_dec x y with
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 30ef8778d..ef3a3a71e 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -5,6 +5,11 @@ Inductive t : Set :=
 
 Print t_rect.
 
+Record A : Type := C { a := 0 : nat; c: nat; b : a=a }.
+
+Eval cbv in fun d:A => match d return 0 = 0 with C a _ b => b end.
+Eval lazy in fun d:A => match d return 0 = 0 with C a _ b => b end.
+
 (* Do not contract nested patterns with dependent return type *)
 (* see bug #1699 *)