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

7 files changed, 24 insertions, 26 deletions

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 =