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

4 files changed, 14 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 57a025e32e..c08972ac15 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 a73c22ee52..d56a375bfe 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 ca17060357..db41809628 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 ea31917701..337eb00472 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