aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-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
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 22:37:51 +0000