diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 4 | ||||
| -rw-r--r-- | kernel/csymtable.ml | 2 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 1 | ||||
| -rw-r--r-- | kernel/inductive.ml | 5 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 1 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | kernel/vconv.ml | 6 | ||||
| -rw-r--r-- | kernel/vm.ml | 1 |
9 files changed, 9 insertions, 15 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index af00edd65..577ea5cb2 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -842,7 +842,7 @@ let strip_update_shift_app head stk = let rec strip_rec rstk h depth = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s - | (Zapp args :: s) as stk -> + | (Zapp args :: s) -> strip_rec (Zapp args :: rstk) {norm=h.norm;term=FApp(h,Array.of_list args)} depth s | Zupdate(m)::s -> @@ -885,7 +885,7 @@ let get_arg h stk = let rec get_args n tys f e stk = match stk with Zupdate r :: s -> - let hd = update r (Cstr,FLambda(n,tys,f,e)) in + let _hd = update r (Cstr,FLambda(n,tys,f,e)) in get_args n tys f e s | Zshift k :: s -> get_args n tys f (subs_shft (k,e)) s diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 73e10df65..f743970c6 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -146,7 +146,6 @@ and slot_for_fv env fv= set_relval rv v; v | VKdef(c,e) -> let v = val_of_constr e c in - let k = nb_rel e in set_relval rv v; v end @@ -158,7 +157,6 @@ and eval_to_patch env (buff,pl,fv) = patch_int buff pos (slot_for_getglobal env kn) in List.iter patch pl; - let nfv = Array.length fv in let vm_env = Array.map (slot_for_fv env) fv in let tc = tcode_of_code buff (length buff) in eval_tcode tc vm_env diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 25464a3ce..67a0f850c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -454,7 +454,6 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = (fun c -> let c = body_of_type c in let sign, rawc = mind_extract_params nparams c in - let env' = push_rel_context sign env in try check_constructors ienv true nparams rawc with IllFormedInd err -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index bf64dfda0..235c82b1a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -593,7 +593,6 @@ let check_one_fix renv recpos def = | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> List.for_all (check_rec_call renv) l && array_for_all (check_rec_call renv) typarray && - let nbfix = Array.length typarray in let decrArg = recindxs.(i) in let renv' = push_fix_renv renv recdef in if (List.length l < (decrArg+1)) then @@ -613,7 +612,7 @@ let check_one_fix renv recpos def = bodies in array_for_all (fun b -> b) ok_vect - | Const kn as c -> + | Const kn -> (try List.for_all (check_rec_call renv) l with (FixGuardError _ ) as e -> if evaluable_constant kn renv.env then @@ -705,7 +704,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = +let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = let (minds, rdef) = inductive_of_mutfix env fix in for i = 0 to Array.length bodies - 1 do let (fenv,body) = rdef.(i) in diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index e0d16d499..c6afb1da0 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -45,7 +45,6 @@ let empty_subst = Umap.empty let add_msid msid mp = Umap.add (MSI msid) (mp,None) let add_mbid mbid mp resolve = - let mp' = MBI mbid in Umap.add (MBI mbid) (mp,resolve) let map_msid msid mp = add_msid msid mp empty_subst diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index f87dc90e4..5ab9f9a02 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -174,7 +174,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 = check_conv cst conv env c1 c2 in cst - | IndType ((kn,i) as ind,mind1) -> + | IndType ((kn,i),mind1) -> Util.error ("The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ diff --git a/kernel/term.ml b/kernel/term.ml index b86ac850c..8bd079ce5 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -748,7 +748,7 @@ let substl laml = substn_many (Array.map make_substituend (Array.of_list laml)) 0 let subst1 lam = substl [lam] -let substl_decl laml (id,bodyopt,typ as d) = +let substl_decl laml (id,bodyopt,typ) = match bodyopt with | None -> (id,None,substl laml typ) | Some body -> (id, Some (substl laml body), type_app (substl laml) typ) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index cdc9fa0f7..8a2ced1d2 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -80,9 +80,9 @@ and conv_whd pb k whd1 whd2 cu = else raise NotConvertible | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom pb k a1 stk1 a2 stk2 cu - | _, Vatom_stk(Aiddef(_,v) as a2,stk) -> + | _, Vatom_stk(Aiddef(_,v),stk) -> conv_whd pb k whd1 (force_whd v stk) cu - | Vatom_stk(Aiddef(_,v) as a1,stk), _ -> + | Vatom_stk(Aiddef(_,v),stk), _ -> conv_whd pb k (force_whd v stk) whd2 cu | _, _ -> raise NotConvertible @@ -343,7 +343,7 @@ let type_of_ind env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_nf_arity -let build_branches_type (mind,_ as ind) mib mip params dep p rtbl = +let build_branches_type (mind,_ as _ind) mib mip params dep p rtbl = (* [build_one_branch i cty] construit le type de la ieme branche (commence a 0) et les lambda correspondant aux realargs *) let build_one_branch i cty = diff --git a/kernel/vm.ml b/kernel/vm.ml index 0aa4f1ff4..8f0d2ebdd 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -318,7 +318,6 @@ let val_of_constant_def n c v = let rec whd_accu a stk = - let n = nargs_of_accu a in let stk = if nargs_of_accu a = 0 then stk else Zapp (args_of_accu a) :: stk in |