aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml6
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/topconstr.ml18
-rw-r--r--interp/topconstr.mli2
-rw-r--r--parsing/g_xml.ml42
-rw-r--r--plugins/subtac/subtac_cases.ml16
-rw-r--r--pretyping/cases.ml13
-rw-r--r--pretyping/detyping.ml14
-rw-r--r--pretyping/detyping.mli4
-rw-r--r--pretyping/glob_term.ml4
-rw-r--r--pretyping/glob_term.mli5
-rw-r--r--pretyping/pattern.ml8
-rw-r--r--pretyping/pattern.mli2
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:47:01 +0000