Glob_term.predicate_pattern: No number of parameters with letins.

Detyping is wrong about it and as far as I understand no one but Constrextern uses
it. Constrextern has now the same machinery for all patterns.

Revert if I miss something.

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

13 files changed, 46 insertions, 50 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 57a025e32..c08972ac1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -727,7 +727,7 @@ let rec extern inctx scopes vars r =
         | Name id, GVar (_,id') when id=id' -> None
         | Name _, _ -> Some (dummy_loc,na) in
       (sub_extern false scopes vars tm,
-       (na',Option.map (fun (loc,ind,_,nal) ->
+       (na',Option.map (fun (loc,ind,nal) ->
 	 let args = List.map (fun x -> CPatAtom (dummy_loc, match x with Anonymous -> None | Name id -> Some (Ident (dummy_loc,id)))) nal in
 	 let full_args = add_patt_for_params ind args in
 	 let c = extern_reference loc vars (IndRef ind) in
@@ -1011,8 +1011,8 @@ let rec glob_of_pat env = function
       in
       let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with
 	| PMeta None, _, _ -> (Anonymous,None),None
-	| _, Some ind, Some (nparams,nargs) ->
-	  return_type_of_predicate ind nparams nargs (glob_of_pat env p)
+	| _, Some ind, Some nargs ->
+	  return_type_of_predicate ind nargs (glob_of_pat env p)
 	| _ -> anomaly "PCase with non-trivial predicate but unknown inductive"
       in
       GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a73c22ee5..d56a375bf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1611,7 +1611,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  let _,args_rel =
 	    list_chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
 	  canonize_args args_rel l (Idset.elements forbidden_names_for_gen) [] [] in
-	match_to_do, Some (cases_pattern_expr_loc t,ind,nparams,List.rev_map snd nal)
+	match_to_do, Some (cases_pattern_expr_loc t,ind,List.rev_map snd nal)
     | None ->
       [], None in
     (tm',(snd na,typ)), extra_id, match_td
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ca1706035..db4180962 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -39,7 +39,7 @@ type aconstr =
   | ABinderList of identifier * identifier * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
   | ACases of case_style * aconstr option *
-      (aconstr * (name * (inductive * int * name list) option)) list *
+      (aconstr * (name * (inductive * name list) option)) list *
       (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
@@ -123,10 +123,10 @@ let glob_constr_of_aconstr_with_binders loc g f e = function
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
-	| Some (ind,npar,nal) ->
+	| Some (ind,nal) ->
 	  let e',nal' = List.fold_right (fun na (e',nal) ->
 	      let e',na' = g e' na in e',na'::nal) nal (e',[]) in
-	  e',Some (loc,ind,npar,nal') in
+	  e',Some (loc,ind,nal') in
 	let e',na' = g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
       let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
@@ -298,8 +298,8 @@ let aconstr_and_vars_of_glob_constr a =
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  Option.iter
-	    (fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
-          (aux tm,(na,Option.map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
+	    (fun (_,_,nl) -> List.iter (add_name found) nl) x;
+          (aux tm,(na,Option.map (fun (_,ind,nal) -> (ind,nal)) x))) tml,
         List.map f eqnl)
   | GLetTuple (loc,nal,(na,po),b,c) ->
       add_name found na;
@@ -440,9 +440,9 @@ let rec subst_aconstr subst bound raw =
       and rl' = list_smartmap
         (fun (a,(n,signopt) as x) ->
 	  let a' = subst_aconstr subst bound a in
-	  let signopt' = Option.map (fun ((indkn,i),n,nal as z) ->
+	  let signopt' = Option.map (fun ((indkn,i),nal as z) ->
 	    let indkn' = subst_ind subst indkn in
-	    if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
+	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
         rl
       and branches' = list_smartmap
@@ -520,11 +520,11 @@ let abstract_return_type_context pi mklam tml rtno =
     rtno
 
 let abstract_return_type_context_glob_constr =
-  abstract_return_type_context (fun (_,_,_,nal) -> nal)
+  abstract_return_type_context (fun (_,_,nal) -> nal)
     (fun na c -> GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evd.InternalHole),c))
 
 let abstract_return_type_context_aconstr =
-  abstract_return_type_context pi3
+  abstract_return_type_context snd
     (fun na c -> ALambda(na,AHole Evd.InternalHole,c))
 
 exception No_match
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index ea3191770..337eb0047 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -35,7 +35,7 @@ type aconstr =
   | ABinderList of identifier * identifier * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
   | ACases of case_style * aconstr option *
-      (aconstr * (name * (inductive * int * name list) option)) list *
+      (aconstr * (name * (inductive * name list) option)) list *
       (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 09af49f62..3cb553437 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -176,7 +176,7 @@ let rec interp_xml_constr = function
       in
       let mat = simple_cases_matrix_of_branches ind brs in
       let nparams,n = compute_inductive_nargs ind in
-      let nal,rtn = return_type_of_predicate ind nparams n p in
+      let nal,rtn = return_type_of_predicate ind n p in
       GCases (loc,RegularStyle,rtn,[tm,nal],mat)
   | XmlTag (loc,"MUTIND",al,[]) ->
       GRef (loc, IndRef (get_xml_inductive al))
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index d60841e72..6893f1351 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -363,7 +363,7 @@ let unify_tomatch_with_patterns isevars env loc typ pats =
 
 let find_tomatch_tycon isevars env loc = function
   (* Try if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind)
+  | Some (_,ind,_) -> mk_tycon (inductive_template isevars env loc ind)
   | None -> empty_tycon
 
 let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
@@ -1414,7 +1414,7 @@ let extract_arity_signature env0 tomatchl tmsign =
       | NotInd (bo,typ) ->
 	  (match t with
 	    | None -> [na,Option.map (lift n) bo,lift n typ]
-	    | Some (loc,_,_,_) ->
+	    | Some (loc,_,_) ->
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
       | IsInd (_,IndType(indf,realargs)) ->
@@ -1423,11 +1423,10 @@ let extract_arity_signature env0 tomatchl tmsign =
 	  let nrealargs = List.length realargs in
 	  let realnal =
 	    match t with
-	      | Some (loc,ind',nparams,realnal) ->
+	      | Some (loc,ind',realnal) ->
 		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type");
-		  if List.length params <> nparams
-		    or nrealargs <> List.length realnal then
+		  if nrealargs <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
@@ -1448,7 +1447,7 @@ let extract_arity_signatures env0 tomatchl tmsign =
       | NotInd (bo,typ) ->
 	  (match t with
 	    | None -> [na,bo,typ]
-	    | Some (loc,_,_,_) ->
+	    | Some (loc,_,_) ->
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
       | IsInd (_,IndType(indf,realargs)) ->
@@ -1456,11 +1455,10 @@ let extract_arity_signatures env0 tomatchl tmsign =
 	  let nrealargs = List.length realargs in
 	  let realnal =
 	    match t with
-	      | Some (loc,ind',nparams,realnal) ->
+	      | Some (loc,ind',realnal) ->
 		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type");
-		  if List.length params <> nparams
-		    or nrealargs <> List.length realnal then
+		  if nrealargs <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d413bfbcd..2b3407c27 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -331,7 +331,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames =
 
 let find_tomatch_tycon evdref env loc = function
   (* Try if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_,realnal) ->
+  | Some (_,ind,realnal) ->
       mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal)
   | None ->
       empty_tycon,None
@@ -1358,7 +1358,7 @@ substituer après par les initiaux *)
 (* builds the matrix of equations testing that each eqn has n patterns
  * and linearizing the _ patterns.
  * Syntactic correctness has already been done in astterm *)
-let matx_of_eqns env tomatchl eqns =
+let matx_of_eqns env eqns =
   let build_eqn (loc,ids,lpat,rhs) =
     let initial_lpat,initial_rhs = lpat,rhs in
     let initial_rhs = rhs in
@@ -1650,7 +1650,7 @@ let extract_arity_signature env0 tomatchl tmsign =
       | NotInd (bo,typ) ->
 	  (match t with
 	    | None -> [na,Option.map (lift n) bo,lift n typ]
-	    | Some (loc,_,_,_) ->
+	    | Some (loc,_,_) ->
  	    user_err_loc (loc,"",
 	    str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
@@ -1660,11 +1660,10 @@ let extract_arity_signature env0 tomatchl tmsign =
 	  let arsign = fst (get_arity env0 indf') in
 	  let realnal =
 	    match t with
-	      | Some (loc,ind',nparams,realnal) ->
+	      | Some (loc,ind',realnal) ->
 		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type.");
-		  if nparams_ctxt <> nparams
-		    or nrealargs_ctxt <> List.length realnal then
+		  if nrealargs_ctxt <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
 	      | None -> list_make nrealargs_ctxt Anonymous in
@@ -1794,7 +1793,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
 let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
 
   (* We build the matrix of patterns and right-hand side *)
-  let matx = matx_of_eqns env tomatchl eqns in
+  let matx = matx_of_eqns env eqns in
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b3daad79e..dc8957dd4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -306,7 +306,7 @@ let it_destRLambda_or_LetIn_names n c =
   in aux n [] c
 
 let detype_case computable detype detype_eqns testdep avoid data p c bl =
-  let (indsp,st,nparams,consnargsl,k) = data in
+  let (indsp,st,consnargsl,k) = data in
   let synth_type = synthetize_type () in
   let tomatch = detype c in
   let alias, aliastyp, pred=
@@ -323,7 +323,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
 	      if List.for_all ((=) Anonymous) nl then None
-	      else Some (dl,indsp,nparams,nl) in
+	      else Some (dl,indsp,nl) in
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
@@ -411,7 +411,7 @@ let rec detype (isgoal:bool) avoid env t =
 	detype_case comp (detype isgoal avoid env)
 	  (detype_eqns isgoal avoid env ci comp)
 	  is_nondep_branch avoid
-	  (ci.ci_ind,ci.ci_pp_info.style,ci.ci_npar,
+	  (ci.ci_ind,ci.ci_pp_info.style,
 	   ci.ci_cstr_ndecls,ci.ci_pp_info.ind_nargs)
 	  (Some p) c bl
     | Fix (nvn,recdef) -> detype_fix isgoal avoid env nvn recdef
@@ -611,9 +611,9 @@ let rec subst_glob_constr subst raw =
         let a' = subst_glob_constr subst a in
         let (n,topt) = x in
         let topt' = Option.smartmap
-          (fun (loc,(sp,i),x,y as t) ->
+          (fun (loc,(sp,i),y as t) ->
             let sp' = subst_ind subst sp in
-            if sp == sp' then t else (loc,(sp',i),x,y)) topt in
+            if sp == sp' then t else (loc,(sp',i),y)) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = list_smartmap
 			(fun (loc,idl,cpl,r as branch) ->
@@ -685,6 +685,6 @@ let simple_cases_matrix_of_branches ind brs =
       (dummy_loc,ids,[p],c))
     brs
 
-let return_type_of_predicate ind nparams nrealargs_ctxt pred =
+let return_type_of_predicate ind nrealargs_ctxt pred =
   let nal,p = it_destRLambda_or_LetIn_names (nrealargs_ctxt+1) pred in
-  (List.hd nal, Some (dummy_loc, ind, nparams, List.tl nal)), Some p
+  (List.hd nal, Some (dummy_loc, ind, List.tl nal)), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 0912a3f23..f9592194c 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -32,7 +32,7 @@ val detype_case :
   (constructor array -> int array -> 'a array ->
     (loc * identifier list * cases_pattern list * glob_constr) list) ->
   ('a -> int -> bool) ->
-  identifier list -> inductive * case_style * int * int array * int ->
+  identifier list -> inductive * case_style * int array * int ->
     'a option -> 'a -> 'a array -> glob_constr
 
 val detype_sort : sorts -> glob_sort
@@ -54,7 +54,7 @@ val it_destRLambda_or_LetIn_names : int -> glob_constr -> name list * glob_const
 val simple_cases_matrix_of_branches :
   inductive -> (int * int * glob_constr) list -> cases_clauses
 val return_type_of_predicate :
-  inductive -> int -> int -> glob_constr -> predicate_pattern * glob_constr option
+  inductive -> int -> glob_constr -> predicate_pattern * glob_constr option
 
 module PrintingInductiveMake :
   functor (Test : sig
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 5922d38dc..616a85444 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -79,7 +79,7 @@ and fix_kind =
   | GCoFix of int
 
 and predicate_pattern =
-    name * (loc * inductive * int * name list) option
+    name * (loc * inductive * name list) option
 
 and tomatch_tuple = (glob_constr * predicate_pattern)
 
@@ -92,7 +92,7 @@ and cases_clauses = cases_clause list
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
-    | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml)
+    | (tm,(na,Some (_,_,nal))) -> na::nal) tml)
 
 let mkGApp loc p t =
   match p with
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index f13d0bee9..a4feac358 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -82,9 +82,8 @@ and fix_kind =
   | GCoFix of int
 
 and predicate_pattern =
-    name * (loc * inductive * int * name list) option
-      (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)], [k]
-	  is the number of parameter of [I]. *)
+    name * (loc * inductive * name list) option
+      (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
 
 and tomatch_tuple = (glob_constr * predicate_pattern)
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 49b63a4b5..0610c00f1 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -30,7 +30,7 @@ type extended_patvar_map = (patvar * constr_under_binders) list
 type case_info_pattern =
     { cip_style : case_style;
       cip_ind : inductive option;
-      cip_ind_args : (int * int) option; (** number of params and args *)
+      cip_ind_args : int option; (** number of args *)
       cip_extensible : bool (** does this match end with _ => _ ? *) }
 
 type constr_pattern =
@@ -133,7 +133,7 @@ let pattern_of_constr sigma t =
         let cip =
 	  { cip_style = ci.ci_pp_info.style;
 	    cip_ind = Some ci.ci_ind;
-	    cip_ind_args = Some (ci.ci_npar, ci.ci_pp_info.ind_nargs);
+	    cip_ind_args = Some (ci.ci_pp_info.ind_nargs);
 	    cip_extensible = false }
 	in
 	let branch_of_constr i c =
@@ -324,13 +324,13 @@ let rec pat_of_raw metas vars = function
 	| _ -> None
       in
       let ind_nargs,ind = match indnames with
-	| Some (_,ind,n,nal) -> Some (n,List.length nal), Some ind
+	| Some (_,ind,nal) -> Some (List.length nal), Some ind
 	| None -> None, get_ind brs
       in
       let ext,brs = pats_of_glob_branches loc metas vars ind brs
       in
       let pred = match p,indnames with
-	| Some p, Some (_,_,_,nal) ->
+	| Some p, Some (_,_,nal) ->
 	  rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p))
 	| _ -> PMeta None
       in
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index cde6d4dc9..e6ec9a498 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -63,7 +63,7 @@ type extended_patvar_map = (patvar * constr_under_binders) list
 type case_info_pattern =
     { cip_style : case_style;
       cip_ind : inductive option;
-      cip_ind_args : (int * int) option; (** number of params and args *)
+      cip_ind_args : int option; (** number of params and args *)
       cip_extensible : bool (** does this match end with _ => _ ? *) }
 
 type constr_pattern =