diff options
75 files changed, 132 insertions, 231 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 9f887fc75..5d2668604 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -151,7 +151,6 @@ END (* Guesses the type and calls field_gen with the right theory *) let field g = Coqlib.check_required_library ["Coq";"field";"Field"]; - let ist = { lfun=[]; debug=get_debug () } in let typ = match Hipattern.match_with_equation (pf_concl g) with | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t diff --git a/contrib/jprover/jall.ml b/contrib/jprover/jall.ml index 876dc6c06..a2a72676c 100644 --- a/contrib/jprover/jall.ml +++ b/contrib/jprover/jall.ml @@ -1788,11 +1788,13 @@ struct else if o = ("",Orr,dummyt,dummyt) then (* Orr is a dummy for no d-gen. rule *) ptree else +(* let (x1,x2,x3,x4) = r and (y1,y2,y3,y4) = o in -(* print_endline ("top or_l: "^x1); + print_endline ("top or_l: "^x1); print_endline ("or_l address: "^addr); - print_endline ("top dgen-rule: "^y1); *) + print_endline ("top dgen-rule: "^y1); +*) trans_add_branch r o addr "" ptree dglist (subrel,tsubrel) (* Isolate layer and outer recursion structure *) @@ -1989,8 +1991,7 @@ struct let (srel,sren) = build_formula_rel dtreelist slist predname in (srel @ rest_rel),(sren @ rest_renlist) | Gamma -> - let n = Array.length suctrees - and succlist = (Array.to_list suctrees) in + let succlist = (Array.to_list suctrees) in let dtreelist = (List.map (fun x -> (1,x)) succlist) in (* if (nonemptys suctrees 0 n) = 1 then let (srel,sren) = build_formula_rel dtreelist slist pos.name in @@ -3039,8 +3040,7 @@ struct if (p.pt = Delta) then (* keep the tree ordering for the successor position only *) let psucc = List.hd succs in let ppsuccs = tpredsucc psucc ftree in - let pre = List.hd ppsuccs - and sucs = List.tl ppsuccs in + let sucs = List.tl ppsuccs in replace_ordering (psucc.name) sucs redpo (* union the succsets of psucc *) else redpo @@ -4582,7 +4582,6 @@ let gen_prover mult_limit logic calculus hyps concls = let (input_map,renamed_termlist) = renam_free_vars (hyps @ concls) in let (ftree,red_ordering,eqlist,(sigmaQ,sigmaJ),ext_proof) = prove mult_limit renamed_termlist logic in let sequent_proof = reconstruct ftree red_ordering sigmaQ ext_proof logic calculus in - let (ptree,count_ax) = bproof sequent_proof in let idl = build_formula_id ftree in (* print_ftree ftree; apple *) (* transform types and rename constants *) diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4 index 8de7f37d3..58307c334 100644 --- a/contrib/jprover/jprover.ml4 +++ b/contrib/jprover/jprover.ml4 @@ -390,7 +390,7 @@ let dyn_truer = (* Do the proof by the guidance of JProver. *) let do_one_step inf = - let (rule, (s1, t1), ((s2, t2) as k)) = inf in + let (rule, (s1, t1), (s2, t2)) = inf in begin (*i if not (Jterm.is_xnil_term t2) then begin diff --git a/contrib/jprover/jtunify.ml b/contrib/jprover/jtunify.ml index 2295e62ce..91aa6b4ba 100644 --- a/contrib/jprover/jtunify.ml +++ b/contrib/jprover/jtunify.ml @@ -177,7 +177,7 @@ let rec combine subst ((ov,oslist) as one_subst) = else (f::rest_combine) -let compose ((n,subst) as sigma) ((ov,oslist) as one_subst) = +let compose ((n,subst) as _sigma) ((ov,oslist) as one_subst) = let com = combine subst one_subst in (* begin print_endline "!!!!!!!!!test print!!!!!!!!!!"; diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index aaabf6533..30562cd44 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -965,7 +965,7 @@ let rec condense p = function let tac',t' = condense (P_APP 2 :: p) t in (tac @ tac'), Oplus(f,t') end - | Oplus(f1,Oz n) as t -> + | Oplus(f1,Oz n) -> let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n) | Oplus(f1,f2) -> if weight f1 = weight f2 then begin @@ -1035,7 +1035,6 @@ let replay_history tactic_normalisation = let p_initial = [P_APP 2;P_TYPE] in let tac = shuffle_cancel p_initial e1.body in let solve_le = - let superieur = Lazy.force coq_SUPERIEUR in let not_sup_sup = mkApp (build_coq_eq (), [| Lazy.force coq_relation; Lazy.force coq_SUPERIEUR; @@ -1095,17 +1094,13 @@ let replay_history tactic_normalisation = tclTHEN (mk_then tac) reflexivity ] | NOT_EXACT_DIVIDE (e1,k) :: l -> - let id = hyp_of_tag e1.id in let c = floor_div e1.constant k in let d = Bigint.sub e1.constant (Bigint.mult c k) in let e2 = {id=e1.id; kind=EQUA;constant = c; body = map_eq_linear (fun c -> c / k) e1.body } in - let eq1 = val_of(decompile e1) - and eq2 = val_of(decompile e2) in + let eq2 = val_of(decompile e2) in let kk = mk_integer k and dd = mk_integer d in - let rhs = mk_plus (mk_times eq2 kk) dd in - let state_eq = mk_eq eq1 rhs in let tac = scalar_norm_add [P_APP 2] e2.body in tclTHENS (cut (mk_gt dd izero)) @@ -1419,8 +1414,6 @@ let coq_omega gl = let coq_omega = solver_time coq_omega let nat_inject gl = - let aux = id_of_string "auxiliary" in - let table = Hashtbl.create 7 in let rec explore p t = try match destructurate_term t with | Kapp(Plus,[t1;t2]) -> diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml index 7b6361afe..69e57ca42 100755 --- a/contrib/omega/omega.ml +++ b/contrib/omega/omega.ml @@ -425,7 +425,7 @@ let redundancy_elimination new_eq_id system = end else begin match optinvert with Some v -> - let kept = + let _kept = if v.constant >? nx.constant then begin add_event (FORGET_I (v.id,nx.id));v end else begin add_event (FORGET_I (nx.id,v.id));nx end in diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml index c22c1dfb5..f554b85f5 100644 --- a/contrib/romega/const_omega.ml +++ b/contrib/romega/const_omega.ml @@ -17,7 +17,6 @@ type result = let destructurate t = let c, args = Term.decompose_app t in - let env = Global.env() in match Term.kind_of_term c, args with | Term.Const sp, args -> Kapp (Names.string_of_id diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 6bc693a13..f1aff8d08 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -604,7 +604,7 @@ let rec condense env = function let tac',t' = condense env t in [do_both (do_list tac) (do_list tac')], Oplus(f,t') end - | (Oplus(f1,Oint n) as t) -> + | Oplus(f1,Oint n) -> let tac,f1' = reduce_factor f1 in [do_left (do_list tac)],Oplus(f1',Oint n) | Oplus(f1,f2) -> diff --git a/ide/coqide.ml b/ide/coqide.ml index 956a275a9..48bb19cb6 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -807,7 +807,7 @@ object(self) goal_nb (if goal_nb<=1 then "" else "s")); List.iter - (fun ((_,_,_,(s,_)) as hyp) -> + (fun ((_,_,_,(s,_)) as _hyp) -> proof_buffer#insert (s^"\n")) hyps; proof_buffer#insert (String.make 38 '_' ^ "(1/"^ @@ -1364,7 +1364,6 @@ Please restart and report NOW."; if Mutex.try_lock c#lock then begin c#clear (); let current_gls = try get_current_goals () with _ -> [] in - let gls_nb = List.length current_gls in let set_goal i (s,t) = let gnb = string_of_int i in @@ -1481,19 +1480,17 @@ Please restart and report NOW."; (input_view#event#connect#key_press self#active_keypress_handler); prerr_endline "CONNECTED active : "; print_id (out_some act_id); - let dir = (match - (out_some ((Vector.get input_views index).analyzed_view)) - #filename - with - | None -> () - | Some f -> - if not (is_in_coq_path f) then - begin - let dir = Filename.dirname f in - ignore (Coq.interp false - (Printf.sprintf "Add LoadPath \"%s\". " dir)) - end) - in () + match + (out_some ((Vector.get input_views index).analyzed_view)) #filename + with + | None -> () + | Some f -> + if not (is_in_coq_path f) then + begin + let dir = Filename.dirname f in + ignore (Coq.interp false + (Printf.sprintf "Add LoadPath \"%s\". " dir)) + end @@ -1832,7 +1829,7 @@ let main files = let load_f () = match select_file ~title:"Load file" () with | None -> () - | (Some f) as fn -> load f + | Some f -> load f in ignore (load_m#connect#activate (load_f)); @@ -1906,7 +1903,7 @@ let main files = let saveall_f () = Vector.iter (function - | {view = view ; analyzed_view = Some av} as full -> + | {view = view ; analyzed_view = Some av} -> begin match av#filename with | None -> () | Some f -> @@ -1929,7 +1926,7 @@ let main files = let revert_f () = Vector.iter (function - {view = view ; analyzed_view = Some av} as full -> + {view = view ; analyzed_view = Some av} -> (try match av#filename,av#stats with | Some f,Some stats -> @@ -2359,7 +2356,7 @@ let main files = let auto_save_f () = Vector.iter (function - {view = view ; analyzed_view = Some av} as full -> + {view = view ; analyzed_view = Some av} -> (try av#auto_save with _ -> ()) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index e8cccf9cc..a71d14c82 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -228,7 +228,7 @@ let rec print_list print fmt = function let browse f url = let l,r = !current.cmd_browse in - let (s,res) = System.run_command try_convert f (l ^ url ^ r) in + let _ = System.run_command try_convert f (l ^ url ^ r) in () let url_for_keyword = diff --git a/ide/undo.ml b/ide/undo.ml index dc723db9d..0b4ea1726 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -107,8 +107,8 @@ object(self) Queue.iter (fun e -> Stack.push e history) redo; Queue.clear redo; end; - let pos = it#offset in -(* if Stack.is_empty history or +(* let pos = it#offset in + if Stack.is_empty history or s=" " or s="\t" or s="\n" or (match Stack.top history with | Insert(old,opos,olen) -> diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index 03ca706c8..275a730b6 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -560,8 +560,8 @@ class font_param_box param = let _ = dialog#connect#destroy GMain.Main.quit in let _ = wb_ok#connect#clicked (fun () -> - let font_opt = dialog#selection#font_name in -(* we#set_text (match font_opt with None -> "" | Some s -> s) ; +(* let font_opt = dialog#selection#font_name in + we#set_text (match font_opt with None -> "" | Some s -> s) ; set_entry_font font_opt;*) dialog#destroy () ) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8faec21df..a3c2a0447 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1306,7 +1306,7 @@ let rec extern_cases_pattern_in_scope scopes vars pat = and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match - | (keyrule,pat,n as rule)::rules -> + | (keyrule,pat,n as _rule)::rules -> try (* Check the number of arguments expected by the notation *) let loc = match t,n with @@ -1718,7 +1718,7 @@ and extern_numeral loc scopes (sc,n) = and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match - | (keyrule,pat,n as rule)::rules -> + | (keyrule,pat,n as _rule)::rules -> let loc = Rawterm.loc_of_rawconstr t in try (* Adjusts to the number of arguments expected by the notation *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 498c483dc..b7be8502d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -337,7 +337,7 @@ let interp_reference vars r = let (r,_,_,_) = intern_reference (Idset.empty,None,[]) (vars,[],[],[],[]) r in r -let apply_scope_env (ids,_,scopes as env) = function +let apply_scope_env (ids,_,scopes) = function | [] -> (ids,None,scopes), [] | sc::scl -> (ids,sc,scopes), scl @@ -415,7 +415,7 @@ let check_or_pat_variables loc ids idsl = (* [merge_aliases] returns the sets of all aliases encountered at this point and a substitution mapping extra aliases to the first one *) -let merge_aliases (ids,subst as aliases) id = +let merge_aliases (ids,subst as _aliases) id = ids@[id], if ids=[] then subst else (id, List.hd ids)::subst let alias_of = function @@ -651,12 +651,12 @@ let merge_impargs l args = | _ -> a::l) l args -let check_projection isproj nargs r = +let check_projection isproj r = match (r,isproj) with | RRef (loc, ref), Some nth -> (try - let n = Recordops.find_projection_nparams ref in - if nargs < nth then + let n = Recordops.find_projection_nparams ref + 1 in + if nth < n then user_err_loc (loc,"",str "Projection has not enough parameters"); with Not_found -> user_err_loc @@ -735,7 +735,7 @@ let rec subst_iterator y t = function | RVar (_,id) as x -> if id = y then t else x | x -> map_rawconstr (subst_iterator y t) x -let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) = +let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) = function | AVar id -> begin @@ -801,15 +801,14 @@ let internalise sigma env allow_soapp lvar c = with Not_found -> raise (InternalisationError (locid,UnboundFixName (false,iddef))) in - let ids' = List.fold_right Idset.add lf ids in let idl = Array.map (fun (id,n,bl,ty,bd) -> - let ((ids'',_,_),rbl) = + let ((ids',_,_),rbl) = List.fold_left intern_local_binder (env,[]) bl in - let ids''' = List.fold_right Idset.add lf ids'' in + let ids'' = List.fold_right Idset.add lf ids' in (List.rev rbl, - intern_type (ids'',tmp_scope,scopes) ty, - intern (ids''',None,scopes) bd)) dl in + intern_type (ids',tmp_scope,scopes) ty, + intern (ids'',None,scopes) bd)) dl in RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n), Array.of_list lf, Array.map (fun (bl,_,_) -> bl) idl, @@ -824,15 +823,14 @@ let internalise sigma env allow_soapp lvar c = with Not_found -> raise (InternalisationError (locid,UnboundFixName (true,iddef))) in - let ids' = List.fold_right Idset.add lf ids in let idl = Array.map (fun (id,bl,ty,bd) -> - let ((ids'',_,_),rbl) = + let ((ids',_,_),rbl) = List.fold_left intern_local_binder (env,[]) bl in - let ids''' = List.fold_right Idset.add lf ids'' in + let ids'' = List.fold_right Idset.add lf ids' in (List.rev rbl, - intern_type (ids'',tmp_scope,scopes) ty, - intern (ids''',None,scopes) bd)) dl in + intern_type (ids',tmp_scope,scopes) ty, + intern (ids'',None,scopes) bd)) dl in RRec (loc,RCoFix n, Array.of_list lf, Array.map (fun (bl,_,_) -> bl) idl, @@ -864,7 +862,7 @@ let internalise sigma env allow_soapp lvar c = intern (ids,None,find_delimiters_scope loc key::scopes) e | CAppExpl (loc, (isproj,ref), args) -> let (f,_,args_scopes,_) = intern_reference env lvar ref in - check_projection isproj (List.length args) f; + check_projection isproj f; RApp (loc, f, intern_args env args_scopes args) | CApp (loc, (isproj,f), args) -> let isproj,f,args = match f with @@ -879,8 +877,9 @@ let internalise sigma env allow_soapp lvar c = let c = intern_notation intern env loc ntn [] in find_appl_head_data lvar c | x -> (intern env f,[],[],[]) in - let args = intern_impargs c env impargs args_scopes (merge_impargs l args) in - check_projection isproj (List.length args) c; + let args = + intern_impargs c env impargs args_scopes (merge_impargs l args) in + check_projection isproj c; (match c with (* Now compact "(f args') args" *) | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) @@ -919,7 +918,7 @@ let internalise sigma env allow_soapp lvar c = RPatVar (loc, n) | CPatVar (loc, (false,n)) when Options.do_translate () -> RVar (loc, n) - | CPatVar (loc, (false,n as x)) -> + | CPatVar (loc, (false,n)) -> if List.mem n (fst (let (a,_,_,_,_) = lvar in a)) & !Options.v7 then RVar (loc, n) else @@ -951,7 +950,7 @@ let internalise sigma env allow_soapp lvar c = ((name_fold Idset.add na ids,ts,sc), (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) - and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) = + and intern_eqn n (ids,tmp_scope,scopes as _env) (loc,lhs,rhs) = let idsl_pll = List.map (intern_cases_pattern scopes ([],[]) None) lhs in let eqn_ids,pll = product_of_cases_patterns [] idsl_pll in diff --git a/interp/genarg.ml b/interp/genarg.ml index f81425eb8..d9afc146b 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -181,24 +181,24 @@ let out_gen t (t',o) = if t = t' then Obj.magic o else failwith "out_gen" let genarg_tag (s,_) = s let fold_list0 f = function - | (List0ArgType t as u, l) -> + | (List0ArgType t, l) -> List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) | _ -> failwith "Genarg: not a list0" let fold_list1 f = function - | (List1ArgType t as u, l) -> + | (List1ArgType t, l) -> List.fold_right (fun x -> f (in_gen t x)) (Obj.magic l) | _ -> failwith "Genarg: not a list1" let fold_opt f a = function - | (OptArgType t as u, l) -> + | (OptArgType t, l) -> (match Obj.magic l with | None -> a | Some x -> f (in_gen t x)) | _ -> failwith "Genarg: not a opt" let fold_pair f = function - | (PairArgType (t1,t2) as u, l) -> + | (PairArgType (t1,t2), l) -> let (x1,x2) = Obj.magic l in f (in_gen t1 x1) (in_gen t2 x2) | _ -> failwith "Genarg: not a pair" diff --git a/interp/notation.ml b/interp/notation.ml index c3903cfc1..7874f95b3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -214,8 +214,6 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,uninterpc) = patl let check_required_module loc sc (ref,d) = - let d' = List.map id_of_string d in - let dir = make_dirpath (List.rev d') in try let _ = sp_of_global ref in () with Not_found -> user_err_loc (loc,"numeral_interpreter", 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 diff --git a/lib/gmap.ml b/lib/gmap.ml index 989c8f22d..4febb3ad1 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -57,7 +57,7 @@ let rec add x data = function Empty -> Node(Empty, x, data, Empty, 1) - | Node(l, v, d, r, h) as t -> + | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in if c = 0 then Node(l, x, data, r, h) @@ -91,7 +91,7 @@ let rec remove x = function Empty -> Empty - | Node(l, v, d, r, h) as t -> + | Node(l, v, d, r, h) -> let c = Pervasives.compare x v in if c = 0 then merge l r diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 7f0def529..91a99b5fb 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -183,7 +183,6 @@ let rec pr_com ft s = (* pretty printing functions *) let pp_dirs ft = - let maxbox = (get_gp ft).max_depth in let pp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n diff --git a/lib/profile.ml b/lib/profile.ml index 1197c92a9..80ae6b4b4 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -259,9 +259,9 @@ let time_overhead_B_C () = for i=1 to loops do try dummy_last_alloc := get_alloc (); - let r = dummy_f dummy_x in - let dw = dummy_spent_alloc () in - let dt = get_time () in + let _r = dummy_f dummy_x in + let _dw = dummy_spent_alloc () in + let _dt = get_time () in () with _ -> assert false done; diff --git a/library/declare.ml b/library/declare.ml index 1b48acf04..bb66d3f26 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -147,7 +147,7 @@ let load_constant i ((sp,kn),(_,_,_,kind)) = let open_constant i ((sp,kn),_) = Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn)) -let cache_constant ((sp,kn),(cdt,dhyps,imps,kind) as o) = +let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) = let id = basename sp in let _,dir,_ = repr_kn kn in if Idmap.mem id !vartab then @@ -211,7 +211,7 @@ let hcons_constant_declaration = function let declare_constant_common id dhyps (cd,kind) = let imps = implicits_flags () in - let (sp,kn as oname) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in + let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in let kn = constant_of_kn kn in kn diff --git a/library/declaremods.ml b/library/declaremods.ml index 69aea75f8..250411e6b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -572,7 +572,6 @@ let library_cache = Hashtbl.create 17 let register_library dir cenv objs digest = let mp = MPfile dir in - let prefix = dir, (mp, empty_dirpath) in let substobjs, objects = try ignore(Global.lookup_module mp); diff --git a/library/impargs.ml b/library/impargs.ml index f41d26c99..abf583d99 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -143,7 +143,7 @@ let update pos rig (na,st) = | Some (DepFlexAndRigid (fpos,rpos) as x) -> if argument_less (pos,fpos) or pos=fpos then DepRigid pos else if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x - | Some (DepFlex fpos as x) -> + | Some (DepFlex fpos) -> if argument_less (pos,fpos) or pos=fpos then DepRigid pos else DepFlexAndRigid (fpos,pos) | Some Manual -> assert false diff --git a/library/lib.ml b/library/lib.ml index b8e7cea95..b1896ae5e 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -50,7 +50,7 @@ let subst_objects prefix subst seg = let classify_segment seg = let rec clean ((substl,keepl,anticipl) as acc) = function | (_,CompilingLibrary _) :: _ | [] -> acc - | ((sp,kn as oname),Leaf o) as node :: stk -> + | ((sp,kn as oname),Leaf o) :: stk -> let id = id_of_label (label kn) in (match classify_object (oname,o) with | Dispose -> clean acc stk diff --git a/library/nametab.ml b/library/nametab.ml index 0ce45c4fb..ddd06c0c2 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -96,7 +96,7 @@ struct [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*) let rec push_until uname o level (current,dirmap) = function - | modid :: path as dir -> + | modid :: path -> let mc = try ModIdmap.find modid dirmap with Not_found -> (Nothing, ModIdmap.empty) @@ -135,7 +135,7 @@ struct let rec push_exactly uname o level (current,dirmap) = function - | modid :: path as dir -> + | modid :: path -> let mc = try ModIdmap.find modid dirmap with Not_found -> (Nothing, ModIdmap.empty) diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index c0207f077..059a93571 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -165,7 +165,6 @@ let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl = let declare_vernac_argument for_v8 loc s cl = let se = mlexpr_of_string s in - let typ = ExtraArgType s in let rawwit = <:expr< $lid:"rawwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index 82e651b4e..f78373c28 100644 --- a/parsing/g_zsyntax.ml +++ b/parsing/g_zsyntax.ml @@ -127,8 +127,6 @@ let inside_printer posneg std_pr p = let pr = if posneg then pr_pos else pr_neg in str "(" ++ pr (std_pr (ope("ZEXPR",[p]))) ++ str ")" in -let outside_zero_printer std_pr p = str "`0`" -in let outside_printer posneg std_pr p = let ((xI,xO,xH),_) = get_z_sign_ast dummy_loc in match (bignat_option_of_pos xI xO xH p) with diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index c016d86f7..1534123f8 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -293,14 +293,14 @@ let rec comment bp = parser bp2 s >] -> comment bp s | [< ''*'; _ = parser - | [< '')' >] ep -> push_string "*)"; + | [< '')' >] -> push_string "*)"; | [< s >] -> real_push_char '*'; comment bp s >] -> () | [< ''"'; s >] -> if Options.do_translate() then (push_string"\"";comm_string bp2 s) else ignore (string bp2 0 s); comment bp s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment - | [< '_ as z; s >] ep -> real_push_char z; comment bp s + | [< '_ as z; s >] -> real_push_char z; comment bp s (* Parse a special token, using the [token_tree] *) @@ -370,7 +370,7 @@ let parse_after_dot bp c strm = len = ident_tail (store (store 0 c1) c2) >] -> ("FIELD", get_buff len) (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *) - | [< ''\226' as c1; t = parse_226_tail + | [< ''\226'; t = parse_226_tail (progress_special '.' (Some !token_tree)) >] ep -> (match t with | TokSymbol (Some t) -> ("", t) @@ -391,7 +391,7 @@ let parse_after_dot bp c strm = len = ident_tail (store (store 0 c1) c2) >] -> ("FIELD", get_buff len) (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *) - | [< ''\226' as c1; t = parse_226_tail + | [< ''\226'; t = parse_226_tail (progress_special '.' (Some !token_tree)) >] ep -> (match t with | TokSymbol (Some t) -> ("", t) @@ -403,7 +403,7 @@ let parse_after_dot bp c strm = (* Parse a token in a char stream *) let rec next_token = parser bp - | [< '' ' | '\t' | '\n' |'\r' as c; s >] ep -> + | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s | [< ''$'; len = ident_tail (store 0 '$') >] ep -> comment_stop bp; @@ -424,7 +424,7 @@ let rec next_token = parser bp comment_stop bp; (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep) (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *) - | [< ''\226' as c1; t = parse_226_tail (Some !token_tree) >] ep -> + | [< ''\226'; t = parse_226_tail (Some !token_tree) >] ep -> comment_stop bp; (match t with | TokSymbol (Some t) -> ("", t), (bp, ep) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 292e981be..90e93b832 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -629,7 +629,7 @@ let find_position forpat other assoc lev = (* Maybe this was (p,Left) and p occurs a second time *) if a = Gramext.LeftA then match l with - | (p,a)::_ as l' when p = n -> raise (Found a) + | (p,a)::_ when p = n -> raise (Found a) | _ -> after := Some pa; pa::(n,create_assoc assoc)::l else (* This was not (p,LeftA) hence assoc is RightA *) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 0dc646198..29501d2a1 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -422,10 +422,8 @@ let pr_extend_gen prgen lev s l = let make_pr_tac (pr_tac_level,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) = let pr_bindings = pr_bindings pr_constr pr_constr in -let pr_bindings_no_with = pr_bindings_no_with pr_constr pr_constr in let pr_with_bindings = pr_with_bindings pr_constr pr_constr in let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in -let pr_constrarg c = spc () ++ pr_constr c in let pr_intarg n = spc () ++ int n in (* Printing tactics as arguments *) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 97139ec15..13d6a62b4 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -495,9 +495,7 @@ let print_name ref = "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object") let print_opaque_name qid = - let sigma = Evd.empty in let env = Global.env () in - let sign = Global.named_context () in match global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in @@ -515,7 +513,6 @@ let print_opaque_name qid = print_named_decl (id,c,ty) let print_about ref = - let sigma = Evd.empty in let k = locate_any_name ref in begin match k with | Term ref -> diff --git a/parsing/search.ml b/parsing/search.ml index 84022e7b1..ec7db4889 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -48,7 +48,6 @@ let rec head_const c = match kind_of_term c with let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = let env = Global.env () in - let imported = Library.opened_libraries() in let crible_rec (sp,_) lobj = match object_tag lobj with | "VARIABLE" -> (try diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 21b96c8a7..a8e47aa9b 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -140,17 +140,6 @@ let new_tac_ext (s,cl) = let declare_tactic_v7 loc s cl = let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in - let hide_tac (_,p,e) = - (* reste a definir les fonctions cachees avec des noms frais *) - let stac = let s = "h_"^s in s.[2] <- Char.lowercase s.[2]; s in - let e = - make_fun - <:expr< - Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ - >> - p in - <:str_item< value $lid:stac$ = $e$ >> - in let se = mlexpr_of_string s in <:str_item< declare @@ -194,7 +183,6 @@ let declare_tactic loc s cl = <:str_item< value $lid:stac$ = $e$ >> in let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in - let se = mlexpr_of_string s in let atomic_tactics = mlexpr_of_list mlexpr_of_string (List.flatten (List.map (fun (al,_) -> is_atomic al) cl')) in diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 6063e9448..942bce798 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -94,7 +94,6 @@ let rec print_script nochange sigma osign pf = (* printed by Show Script command *) let print_treescript nochange sigma _osign pf = let rec aux top pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in match pf.ref with | None -> if nochange then diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 79b048979..28e8c4139 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -427,7 +427,7 @@ let unify_tomatch_with_patterns isevars env tmloc typ = function | Some (cloc,(cstr,_ as c)) -> (let tyi = inductive_of_constructor c in try - let indtyp = inh_coerce_to_ind isevars env tmloc typ tyi in + let _indtyp = inh_coerce_to_ind isevars env tmloc typ tyi in IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ) with NotCoercible -> (* 2 cases : Not the right inductive or not an inductive at all *) @@ -782,7 +782,6 @@ let build_aliases_context env sigma names allpats pats = let newallpats = List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in let oldallpats = List.map List.tl oldallpats in - let u = Retyping.get_type_of env sigma deppat in let decl = (na,Some deppat,t) in let a = (deppat,nondeppat,d,t) in insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1) @@ -918,7 +917,6 @@ let abstract_conclusion typ cs = lam_it p sign let infer_predicate loc env isevars typs cstrs indf = - let (mis,_) = dest_ind_family indf in (* Il faudra substituer les isevars a un certain moment *) if Array.length cstrs = 0 then (* "TODO4-3" *) error "Inference of annotation for empty inductive types not implemented" @@ -930,7 +928,10 @@ let infer_predicate loc env isevars typs cstrs indf = in let eqns = array_map2 prepare_unif_pb typs cstrs in (* First strategy: no dependencies at all *) -(* let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in*) +(* + let (mis,_) = dest_ind_family indf in + let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in +*) let (sign,_) = get_arity env indf in let mtyp = if array_exists is_Type typs then @@ -980,7 +981,7 @@ let rec map_predicate f k = function let rec noccurn_predicate k = function | PrCcl ccl -> noccurn k ccl | PrProd pred -> noccurn_predicate (k+1) pred - | PrLetIn ((names,dep as tm),pred) -> + | PrLetIn ((names,dep),pred) -> let k' = List.length names + (if dep<>Anonymous then 1 else 0) in noccurn_predicate (k+k') pred @@ -1191,7 +1192,7 @@ let group_equations pb mind current cstrs mat = let rest = {rest with tag = lower_pattern_status rest.tag} in brs.(i-1) <- (args, rest) :: brs.(i-1) done - | PatCstr (loc,((_,i) as cstr),args,_) as pat -> + | PatCstr (loc,((_,i)),args,_) -> (* This is a regular clause *) only_default := false; brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in @@ -1240,8 +1241,6 @@ let build_branch current deps pb eqns const_info = else DepAlias in - let partialci = - applist (mkConstruct const_info.cs_cstr, const_info.cs_params) in let history = push_history_pattern const_info.cs_nargs (AliasConstructor const_info.cs_cstr) @@ -1339,7 +1338,7 @@ and match_current pb ((current,typ as ct),deps) = if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt then compile (shift_problem ct pb) else - let constraints = Array.map (solve_constraints indt) cstrs in + let _constraints = Array.map (solve_constraints indt) cstrs in (* We generalize over terms depending on current term to match *) let pb = generalize_problem pb current deps in @@ -1444,7 +1443,7 @@ let prepare_initial_alias_eqn isdep tomatchl eqn = (fun pat (tm,tmtyp) (subst, stripped_pats) -> match alias_of_pat pat with | Anonymous -> (subst, pat::stripped_pats) - | Name idpat as na -> + | Name idpat -> match kind_of_term tm with | Rel n when not (is_dependent_indtype tmtyp) & not isdep -> (n, idpat)::subst, (unalias_pat pat::stripped_pats) diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 1eccc645d..cc3725210 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -100,7 +100,6 @@ let clenv_environments_evars env evd bound c = | (n, Prod (na,c1,c2)) -> let e',constr = Evarutil.new_evar e env c1 in let dep = dependent (mkRel 1) c2 in - let na' = if dep then na else Anonymous in clrec (e', constr::ts) (option_app ((+) (-1)) n) (if dep then (subst1 constr c2) else c2) | (n, LetIn (na,b,_,c)) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 835f1e00d..a0c605857 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -78,7 +78,7 @@ let evar_apprec_nobeta env isevars stack c = let evar_apprec env isevars stack c = let sigma = evars_of isevars in let rec aux s = - let (t,stack as s') = Reductionops.apprec env sigma s in + let (t,stack) = Reductionops.apprec env sigma s in match kind_of_term t with | Evar (n,_ as ev) when Evd.is_defined sigma n -> aux (Evd.existential_value sigma ev, stack) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index ce8aa4844..12559d1da 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -183,7 +183,7 @@ let make_evar_instance_with_rel env = let make_subst env args = snd (fold_named_context - (fun env (id,b,c) (args,l as g) -> + (fun env (id,b,c) (args,l) -> match b, args with | (* None *) _ , a::rest -> (rest, (id,a)::l) (* | Some _, _ -> g*) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e58609195..ea21efcc4 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -248,7 +248,6 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let mis_make_indrec env sigma listdepkind mib = let nparams = mib.mind_nparams in let nparrec = mib. mind_nparams_rec in - let lnamespar = mib.mind_params_ctxt in let lnonparrec,lnamesparrec = list_chop (nparams-nparrec) mib.mind_params_ctxt in let nrec = List.length listdepkind in @@ -380,7 +379,6 @@ let mis_make_indrec env sigma listdepkind mib = let recarg = (dest_subterms recargsvec.(tyi)).(j) in let recarg = recargpar@recarg in let vargs = extended_rel_list (nrec+i+j) lnamesparrec in - let indf = (indi, vargs) in let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in let p_0 = type_rec_branch @@ -532,7 +530,6 @@ let type_rec_branches recursive env sigma indt p c = let tyi = snd ind in let init_depPvec i = if i = tyi then Some(true,p) else None in let depPvec = Array.init mib.mind_ntypes init_depPvec in - let vargs = Array.of_list params in let constructors = get_constructors env indf in let lft = array_map2 diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index c540a4a1f..d0dca036e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -194,7 +194,6 @@ let build_dependent_constructor cs = let build_dependent_inductive env ((ind, params) as indf) = let arsign,_ = get_arity env indf in - let (mib,mip) = Inductive.lookup_mind_specif env ind in let nrealargs = List.length arsign in applist (mkInd ind, diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 6e06f978f..c67917477 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -129,7 +129,7 @@ let rec inst lvar = function (* Non recursive *) | (PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x (* Bound to terms *) - | (PFix _ | PCoFix _ as r) -> + | (PFix _ | PCoFix _) -> error ("Not instantiable pattern") let rec subst_pattern subst pat = match pat with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 497739692..148be3991 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -403,7 +403,7 @@ let rec pretype tycon env isevars lvar = function | RLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env isevars lvar c in - let (IndType (indf,realargs) as indt) = + let (IndType (indf,realargs)) = try find_rectype env (evars_of !isevars) cj.uj_type with Not_found -> let cloc = loc_of_rawconstr c in @@ -441,7 +441,6 @@ let rec pretype tycon env isevars lvar = function let mis,_ = dest_ind_family indf in let ci = make_default_case_info env LetStyle mis in mkCase (ci, p, cj.uj_val,[|f|]) in - let cs = build_dependent_constructor cs in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } | None -> @@ -550,7 +549,6 @@ let rec pretype tycon env isevars lvar = function else pretype (mk_tycon bty.(0)) env isevars lvar f in let fv = fj.uj_val in - let ft = fj.uj_type in let v = let mis,_ = dest_ind_family indf in let ci = make_default_case_info env st mis in @@ -661,7 +659,7 @@ let rec pretype tycon env isevars lvar = function | RIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env isevars lvar c in - let (IndType (indf,realargs) as indt) = + let (IndType (indf,realargs)) = try find_rectype env (evars_of !isevars) cj.uj_type with Not_found -> let cloc = loc_of_rawconstr c in @@ -799,8 +797,6 @@ let rec pretype tycon env isevars lvar = function let (ind,params) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let recargs = mip.mind_recargs in - let mI = mkInd ind in - let nconstr = Array.length mip.mind_consnames in let tyi = snd ind in if isrec && mis_is_recursive_subset [tyi] recargs then Some (Detyping.detype (false,env) @@ -976,7 +972,7 @@ let check_evars env initial_sigma isevars c = let sigma = evars_of !isevars in let rec proc_rec c = match kind_of_term c with - | Evar (ev,args as k) -> + | Evar (ev,args) -> assert (Evd.in_dom sigma ev); if not (Evd.in_dom initial_sigma ev) then let (loc,k) = evar_source ev !isevars in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7476dc0a7..67c0fc856 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -188,7 +188,7 @@ let contract_cofix (bodynum,(types,names,bodies as typedbodies)) = let reduce_mind_case mia = match kind_of_term mia.mconstr with - | Construct (ind_sp,i as cstr_sp) -> + | Construct (ind_sp,i) -> (* let ncargs = (fst mia.mci).(i-1) in*) let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1),real_cargs) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 117b626ea..c9189ad2f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -224,7 +224,7 @@ let compute_consteval_mutual_fix sigma env ref = match kind_of_term c' with | Lambda (na,t,g) when l=[] -> srec (push_rel (na,None,t) env) (minarg+1) (t::labs) ref g - | Fix ((lv,i),(names,_,_) as fix) -> + | Fix ((lv,i),(names,_,_)) -> (* Last known constant wrapping Fix is ref = [labs](Fix l) *) (match compute_consteval_direct sigma env ref with | NotAnElimination -> (*Above const was eliminable but this not!*) @@ -360,7 +360,7 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) = let reduce_mind_case_use_function func env mia = match kind_of_term mia.mconstr with - | Construct(ind_sp,i as cstr_sp) -> + | Construct(ind_sp,i) -> let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1), real_cargs) | CoFix (_,(names,_,_) as cofix) -> @@ -592,7 +592,6 @@ let is_head c t = let contextually byhead (locs,c) f env sigma t = let maxocc = List.fold_right max locs 0 in let pos = ref 1 in - let check = ref true in let except = List.exists (fun n -> n<0) locs in if except & (List.exists (fun n -> n>=0) locs) then error "mixing of positive and negative occurences" @@ -799,7 +798,7 @@ let pattern_occs loccs_trm env sigma c = exception NotStepReducible let one_step_reduce env sigma c = - let rec redrec (x, largs as s) = + let rec redrec (x, largs) = match kind_of_term x with | Lambda (n,t,c) -> (match decomp_stack largs with diff --git a/pretyping/termops.ml b/pretyping/termops.ml index ee1bfe4d6..1a6521d98 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -614,7 +614,6 @@ let replace_term = replace_term_gen eq_constr let subst_term_occ_gen locs occ c t = let maxocc = List.fold_right max locs 0 in let pos = ref occ in - let check = ref true in let except = List.exists (fun n -> n<0) locs in if except & (List.exists (fun n -> n>=0) locs) then error "mixing of positive and negative occurences" diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 303338143..3db11ce39 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -30,7 +30,6 @@ let w_refine env ev rawc evd = let sigma,typed_c = Pretyping.understand_gen_tcc (evars_of evd) env [] (Some e_info.evar_concl) rawc in - let inst_info = {e_info with evar_body = Evar_defined typed_c } in evar_define ev typed_c (evars_reset_evd sigma evd) (* vernac command Existential *) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6da2c8c2f..8e02a7b27 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -79,7 +79,7 @@ let make_flag f = in red let is_reference c = - try let r = global_of_constr c in true with _ -> false + try let _ref = global_of_constr c in true with _ -> false let red_expr_tab = ref Stringmap.empty diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 37dc016c9..816fdf932 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -217,7 +217,7 @@ let mutual_cofix f others gl = with_check (refiner (Prim (Cofix (f,others)))) gl let rename_bound_var_goal gls = - let { evar_hyps = sign; evar_concl = cl } as gl = sig_it gls in + let { evar_hyps = sign; evar_concl = cl } = sig_it gls in let ids = ids_of_named_context sign in convert_concl_no_check (rename_bound_var (Global.env()) ids cl) gls diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 3808cbe10..784bbdc3d 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -198,7 +198,6 @@ let clean file = let all_modules_in_dir dir = try let lst = ref [] - and stg = ref "" and dh = Unix.opendir dir in try while true do diff --git a/tactics/auto.ml b/tactics/auto.ml index 0fda09a9a..dd07c2b90 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -670,7 +670,7 @@ and my_find_search db_list local_db hdc concl = (local_db::db_list) in List.map - (fun ({pri=b; pat=p; code=t} as patac) -> + (fun {pri=b; pat=p; code=t} -> (b, match t with | Res_pf (term,cl) -> unify_resolve (term,cl) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 79753ac73..52f5f011a 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -74,8 +74,7 @@ let e_constructor_tac boundopt i lbind gl = let cl = pf_concl gl in let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in let nconstr = - Array.length (snd (Global.lookup_inductive mind)).mind_consnames - and sigma = project gl in + Array.length (snd (Global.lookup_inductive mind)).mind_consnames in if i=0 then error "The constructors are numbered starting from 1"; if i > nconstr then error "Not enough constructors"; begin match boundopt with @@ -217,7 +216,7 @@ and e_my_find_search db_list local_db hdc concl = list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list) in let tac_of_hint = - fun ({pri=b; pat = p; code=t} as patac) -> + fun {pri=b; pat = p; code=t} -> (b, let tac = match t with diff --git a/tactics/elim.ml b/tactics/elim.ml index 6a91cbc94..90b3c66b2 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -181,7 +181,6 @@ let double_ind h1 h2 gls = if abs_i < abs_j then (abs_i,abs_j) else if abs_i > abs_j then (abs_j,abs_i) else error "Both hypotheses are the same" in - let cl = pf_concl gls in (tclTHEN (tclDO abs_i intro) (onLastHyp (fun id -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 4797146a3..57d9ab58a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -314,7 +314,7 @@ let discriminable env sigma t1 t2 = the continuation then constructs the case-split. *) let descend_then sigma env head dirn = - let IndType (indf,_) as indt = + let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) with Not_found -> assert false in let ind,_ = dest_ind_family indf in @@ -357,7 +357,7 @@ let descend_then sigma env head dirn = giving [True], and all the rest giving False. *) let construct_discriminator sigma env dirn c sort = - let (IndType(indf,_) as indt) = + let IndType(indf,_) = try find_rectype env sigma (type_of env sigma c) with Not_found -> (* one can find Rel(k) in case of dependent constructors @@ -392,7 +392,6 @@ let rec build_discriminator sigma env dirn c sort = function try find_rectype env sigma cty with Not_found -> assert false in let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in - let _,arsort = get_arity env indf in let nparams = mib.mind_nparams in let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in let newc = mkRel(cnum_nlams-(argnum-nparams)) in @@ -434,7 +433,6 @@ let discrEq (lbeq,(t,t1,t2)) id gls = let e_env = push_named (e,None,t) env in let discriminator = build_discriminator sigma e_env dirn (mkVar e) sort cpath in - let (indt,_) = find_mrectype env sigma t in let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq gls in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index c3735b2c8..b91222ae9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -300,7 +300,7 @@ let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref let match_sigma ex ex_pat = match matches (Lazy.force ex_pat) ex with - | [(m1,a);(m2,p);(m3,car);(m4,cdr)] as l -> + | [(m1,a);(m2,p);(m3,car);(m4,cdr)] -> assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4); (a,p,car,cdr) | _ -> diff --git a/tactics/inv.ml b/tactics/inv.ml index 75cb66778..57630c964 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -134,7 +134,6 @@ let make_inv_predicate env sigma indf realargs id status concl = else make_iterated_tuple env' sigma ai (xi,ti) in - let sort = get_sort_of env sigma concl in let eq_term = Coqlib.build_coq_eq () in let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist @@ -305,7 +304,6 @@ let remember_first_eq id x = if !x = None then x := Some id a rewrite rule. It erases the clause which is given as input *) let projectAndApply thin id eqname names depids gls = - let env = pf_env gls in let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id))) (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) @@ -400,7 +398,6 @@ let rewrite_equations othin neqns names ba gl = let (depids,nodepids) = split_dep_and_nodep ba.assums gl in let rewrite_eqns = let first_eq = ref None in - let update id = if !first_eq = None then first_eq := Some id in match othin with | Some thin -> tclTHENSEQ diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 1a221dd16..60d05ec70 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -263,8 +263,8 @@ let inversion_lemma_from_goal n na id sort dep_option inv_op = let gl = nth_goal_of_pftreestate n pts in let t = pf_get_hyp_typ gl id in let env = pf_env gl and sigma = project gl in - let fv = global_vars env t in (* Pourquoi ??? + let fv = global_vars env t in let thin_ids = thin_ids (hyps,fv) in if not(list_subset thin_ids fv) then errorlabstrm "lemma_inversion" diff --git a/tactics/refine.ml b/tactics/refine.ml index d53310c66..493232d3c 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -251,7 +251,7 @@ let rec compute_metamap env c = match kind_of_term c with * Réalise le 3. ci-dessus *) -let rec tcc_aux subst (TH (c,mm,sgp) as th) gl = +let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = let c = substl subst c in match (kind_of_term c,sgp) with (* mv => sous-but : on ne fait rien *) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 3db8be9dc..5cd163364 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -527,7 +527,6 @@ let what_edited id = let check_is_dependent n args_ty output = let m = List.length args_ty - n in let args_ty_quantifiers, args_ty = Util.list_chop n args_ty in - let delift n = substl (Array.to_list (Array.make n (mkRel 1) (* dummy *))) in let rec aux m t = match kind_of_term t with Prod (n,s,t) when m > 0 -> @@ -648,7 +647,6 @@ let apply_to_relation subst rel = mkApp (rel.rel_Xreflexive_relation_class, subst) } let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = - let env = Global.env() in let lem = match lemma_infos with None -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 79b3b330d..5948da2b8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -385,7 +385,6 @@ let adjust_loc loc = if !strict_check then dummy_loc else loc (* Globalize a name which must be bound -- actually just check it is bound *) let intern_hyp ist (loc,id as locid) = - let (_,env) = get_current_context () in if not !strict_check then locid else if find_ident id ist then @@ -396,7 +395,7 @@ let intern_hyp ist (loc,id as locid) = let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id) let intern_int_or_var ist = function - | ArgVar locid as x -> ArgVar (intern_hyp ist locid) + | ArgVar locid -> ArgVar (intern_hyp ist locid) | ArgArg n as x -> x let intern_inductive ist = function @@ -404,7 +403,7 @@ let intern_inductive ist = function | r -> ArgArg (Nametab.global_inductive r) let intern_global_reference ist = function - | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id) + | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) | r -> let loc,qid = qualid_of_reference r in try ArgArg (loc,locate_global qid) @@ -497,7 +496,7 @@ let intern_clause_pattern ist (l,occl) = let intern_induction_arg ist = function | ElimOnConstr c -> ElimOnConstr (intern_constr ist c) | ElimOnAnonHyp n as x -> x - | ElimOnIdent (loc,id) as x -> + | ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) ElimOnConstr (intern_constr ist (CRef (Ident (dummy_loc,id)))) @@ -506,7 +505,7 @@ let intern_induction_arg ist = function (* Globalizes a reduction expression *) let intern_evaluable ist = function - | Ident (loc,id) as r when find_ltacvar id ist -> ArgVar (loc,id) + | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id) | Ident (_,id) when (not !strict_check & find_hyp id ist) or find_ctxvar id ist -> ArgArg (EvalVarRef id, None) @@ -749,8 +748,6 @@ let rec intern_atomic lf ist x = let _ = lookup_tactic opn in TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l) | TacAlias (loc,s,l,(dir,body)) -> - let (l1,l2) = ist.ltacvars in - let ist' = { ist with ltacvars = ((List.map fst l)@l1,l2) } in let l = List.map (fun (id,a) -> (strip_meta id,intern_genarg ist a)) l in try TacAlias (loc,s,l,(dir,body)) with e -> raise (locate_error_in_file (string_of_dirpath dir) e) @@ -1036,7 +1033,7 @@ let get_debug () = !debug let interp_ident ist id = try match List.assoc id ist.lfun with | VIntroPattern (IntroIdentifier id) -> id - | VConstr c as v when isVar c -> + | VConstr c when isVar c -> (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *) (* c is then expected not to belong to the proof context *) (* would be checkable if env were known from interp_ident *) @@ -1048,7 +1045,7 @@ let interp_ident ist id = let interp_intro_pattern_var ist id = try match List.assoc id ist.lfun with | VIntroPattern ipat -> ipat - | VConstr c as v when isVar c -> + | VConstr c when isVar c -> (* This happends e.g. in definitions like "Tac H = Clear H; Intro H" *) (* c is then expected not to belong to the proof context *) (* would be checkable if env were known from interp_ident *) @@ -1076,7 +1073,7 @@ let is_variable env id = List.mem id (ids_of_named_context (Environ.named_context env)) let variable_of_value env = function - | VConstr c as v when isVar c -> destVar c + | VConstr c when isVar c -> destVar c | VIntroPattern (IntroIdentifier id) when is_variable env id -> id | _ -> raise Not_found diff --git a/tactics/tactics.ml b/tactics/tactics.ml index abb86ffde..5079a1010 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -871,8 +871,7 @@ let constructor_tac boundopt i lbind gl = let cl = pf_concl gl in let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in let nconstr = - Array.length (snd (Global.lookup_inductive mind)).mind_consnames - and sigma = project gl in + Array.length (snd (Global.lookup_inductive mind)).mind_consnames in if i=0 then error "The constructors are numbered starting from 1"; if i > nconstr then error "Not enough constructors"; begin match boundopt with @@ -1373,7 +1372,7 @@ let cook_sign hyp0 indvars env = in let _ = fold_named_context seek_deps env ~init:None in (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) - let compute_lstatus lhyp (hyp,_,_ as d) = + let compute_lstatus lhyp (hyp,_,_) = if hyp = hyp0 then raise (Shunt lhyp); if List.mem hyp !ldeps then begin lstatus := (hyp,lhyp)::!lstatus; @@ -1476,7 +1475,6 @@ let error_ind_scheme s = (* Check that the elimination scheme has a form similar to the elimination schemes built by Coq *) let compute_elim_signature elimt names_info = - let nparams = ref 0 in let hyps,ccl = decompose_prod_assum elimt in let n = List.length hyps in if n = 0 then error_ind_scheme ""; @@ -1895,7 +1893,6 @@ let interpretable_as_section_decl d1 d2 = match d1,d2 with | (_,None,t1), (_,_,t2) -> eq_constr t1 t2 let abstract_subproof name tac gls = - let env = Global.env() in let current_sign = Global.named_context() and global_sign = pf_hyps gls in let sign,secsign = @@ -1923,7 +1920,6 @@ let abstract_subproof name tac gls = in (* Faudrait un peu fonctionnaliser cela *) let cd = Entries.DefinitionEntry const in let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in - let newenv = Global.env() in constr_of_global (ConstRef con) in exact_no_check @@ -1940,7 +1936,6 @@ let tclABSTRACT name_op tac gls = let admit_as_an_axiom gls = - let env = Global.env() in let current_sign = Global.named_context() and global_sign = pf_hyps gls in let sign,secsign = diff --git a/toplevel/class.ml b/toplevel/class.ml index 88983637a..eb767694b 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -268,8 +268,6 @@ lorque source est None alors target est None aussi. let add_new_coercion_core coef stre source target isid = check_source source; - let env = Global.env () in - let v = constr_of_global coef in let t = Global.type_of_global coef in if coercion_exists coef then raise (CoercionError AlreadyExists); let tg,lp = prods_of t in diff --git a/toplevel/command.ml b/toplevel/command.ml index 2da3e2cf5..0a97baf8b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -171,7 +171,7 @@ let assumption_message id = let declare_one_assumption is_coe (local,kind) c (_,ident) = let r = match local with | Local when Lib.sections_are_opened () -> - let r = + let _ = declare_variable ident (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in assumption_message ident; @@ -279,8 +279,7 @@ let interp_mutual lparams lnamearconstrs finite = [] lnamearconstrs in if not (list_distinct allnames) then error "Two inductive objects have the same name"; - let nparams = local_binders_length lparams - and sigma = Evd.empty + let sigma = Evd.empty and env0 = Global.env() in let env_params, params = List.fold_left @@ -313,8 +312,6 @@ let interp_mutual lparams lnamearconstrs finite = let paramassums = List.fold_right (fun d l -> match d with (id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in - let indnames = - List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in let nparamassums = List.length paramassums in let (ind_env,ind_impls,arityl) = List.fold_left @@ -432,7 +429,7 @@ let extract_coe_la_lc = function let build_mutual lind finite = let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in let notations,mie = interp_mutual lparams lnamearconstructs finite in - let kn = declare_mutual_with_eliminations false mie in + let _ = declare_mutual_with_eliminations false mie in (* Declare the notations now bound to the inductive types *) List.iter (fun (df,c,scope) -> Metasyntax.add_notation_interpretation df [] c scope) notations; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cc3740501..56f6b111e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -129,7 +129,6 @@ let re_exec is_ide = let s = !re_exec_version in let is_native = (Mltop.get()) = Mltop.Native in let prog = Sys.argv.(0) in - let coq = Filename.basename prog in if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin let s = if s = "" then if is_native then "opt" else "byte" else s in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 8b72d5b01..55201ea43 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -84,7 +84,6 @@ let explain_elim_arity ctx ind aritylst c pj okinds = let ctx = make_all_name_different ctx in let pi = pr_inductive ctx ind in let pc = prterm_env ctx c in - let ppt = prterm_env ctx pj.uj_type in let msg = match okinds with | Some(kp,ki,explanation) -> let pki = prterm_env ctx ki in @@ -380,7 +379,6 @@ let explain_var_not_found ctx id = spc () ++ str "in the current" ++ spc () ++ str "environment" let explain_wrong_case_info ctx ind ci = - let ctx = make_all_name_different ctx in let pi = prterm (mkInd ind) in if ci.ci_ind = ind then str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++ @@ -646,8 +644,8 @@ let explain_needs_inversion ctx x t = px ++ str " of type: " ++ pt let explain_unused_clause env pats = - let s = if List.length pats > 1 then "s" else "" in (* Without localisation + let s = if List.length pats > 1 then "s" else "" in (str ("Unused clause with pattern"^s) ++ spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")") *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a99a15b35..498b21f7f 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -201,7 +201,6 @@ let check_entry_type (u,n) = | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries" let add_grammar_obj univ entryl = - let u = create_univ_if_new univ in let g = interp_grammar_command univ check_entry_type entryl in Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g)) @@ -662,12 +661,12 @@ let read_recursive_format sl fmt = let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) -let hunks_of_format (from,(vars,typs) as vt) symfmt = +let hunks_of_format (from,(vars,typs)) symfmt = let rec aux = function | symbs, (UnpTerminal s' as u) :: fmt when s' = String.make (String.length s') ' ' -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt + | Terminal s :: symbs, (UnpTerminal s') :: fmt when s = unquote_notation_token s' -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' -> @@ -811,7 +810,6 @@ let pr_arg_level from = function | (n,_) -> str "Unknown level" let pr_level ntn (from,args) = - let lopen = ntn.[0] = '_' and ropen = ntn.[String.length ntn - 1] = '_' in (* let ppassoc, args = match args with | [] -> mt (), [] @@ -1350,7 +1348,6 @@ let add_notation local c dfmod mv8 sc = add_notation_in_scope local df c modifiers mv8 sc toks | Some n -> (* Declare both syntax and interpretation *) - let assoc = match assoc with None -> Some Gramext.NonA | a -> a in add_notation_in_scope local df c modifiers mv8 sc toks (* TODO add boxes information in the expression *) @@ -1410,7 +1407,6 @@ let add_infix local (inf,modl) pr mv8 sc = let (recs,vars,symbs) = analyse_notation_tokens toks in let (acvars,ac) = interp_aconstr [] vars a in let a' = (remove_vars recs acvars,ac) in - let a_for_old = interp_global_rawconstr_with_vars vars a in add_notation_interpretation_core local symbs None df a' sc onlyparse true None else diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 926d3e73b..124ad03c6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -64,7 +64,6 @@ let cl_of_qualid = function let show_proof () = let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts in let cursor = cursor_of_pftreestate pts in let evc = evc_of_pftreestate pts in let (pfterm,meta_types) = extract_open_pftreestate pts in @@ -1096,8 +1095,7 @@ let vernac_show = function let vernac_check_guard () = let pts = get_pftreestate () in - let pf = proof_of_pftreestate pts - and cursor = cursor_of_pftreestate pts in + let pf = proof_of_pftreestate pts in let (pfterm,_) = extract_open_pftreestate pts in let message = try diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index e5d7d75bd..a8d0b1390 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -211,9 +211,6 @@ let pr_opt_hintbases l = match l with let pr_hints local db h pr_c pr_pat = let opth = pr_opt_hintbases db in - let pr_aux = function - | CAppExpl (_,(_,qid),[]) -> pr_reference qid - | _ -> mt () in let pph = match h with | HintsResolve l -> @@ -604,8 +601,6 @@ let rec pr_vernac = function str"Eval" ++ spc() ++ pr_red_expr (pr_constr, pr_lconstr, pr_reference) r ++ str" in" ++ spc() in - let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) in - let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) in let pr_def_body = function | DefineBody (bl,red,c,d) -> let (bl2,body,ty) = match d with @@ -654,8 +649,7 @@ let rec pr_vernac = function (* Copie simplifiée de command.ml pour recalculer les implicites, *) (* les notations, et le contexte d'evaluation *) let lparams = match l with [] -> assert false | (_,_,la,_,_)::_ -> la in - let nparams = local_binders_length lparams - and sigma = Evd.empty + let sigma = Evd.empty and env0 = Global.env() in let (env_params,params) = List.fold_left @@ -684,12 +678,10 @@ let rec pr_vernac = function (env', (recname,impls)::ind_impls, (arity::arl))) (env0, [], []) l in - let lparnames = List.map (fun (na,_,_) -> na) params in let notations = List.fold_right (fun (_,ntnopt,_,_,_) l ->option_cons ntnopt l) l [] in let ind_env_params = Environ.push_rel_context params ind_env in - let lparnames = List.map (fun (na,_,_) -> na) params in let impl = List.map (fun ((_,recname),_,_,arityc,_) -> let arity = Constrintern.interp_type sigma env_params arityc in |