From f8b5525eea31c226dfb2ebdc22be512f8af2ebbe Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 8 Apr 2009 17:23:13 +0000 Subject: Some dead code removal + cleanups This commit concerns about the first half of the useless code mentionned by Oug for coqtop (without plugins). For the moment, Oug is used in a mode where any elements mentionned in a .mli is considered to be precious. This already allows to detect and remove about 600 lines, and more is still to come. Among the interesting points, the type Entries.specification_entry and its constructors SPExxx were never used. Large parts of cases.ml (and hence subtac_cases.ml) were also useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/closure.ml | 11 ---- interp/constrextern.ml | 50 ----------------- interp/constrintern.ml | 18 ------- interp/dumpglob.ml | 10 ---- kernel/closure.ml | 11 ---- kernel/conv_oracle.ml | 8 --- kernel/entries.ml | 11 +--- kernel/entries.mli | 11 +--- kernel/environ.ml | 6 --- kernel/names.ml | 8 +-- kernel/retroknowledge.ml | 18 ++----- kernel/univ.ml | 41 +++++++------- lib/bigint.ml | 4 -- library/declare.ml | 6 +-- library/declaremods.ml | 11 ++-- library/decls.ml | 4 -- library/goptions.ml | 7 ++- library/heads.ml | 8 +-- library/libnames.ml | 2 - library/libobject.mli | 2 +- parsing/g_constr.ml4 | 4 -- parsing/g_vernac.ml4 | 5 -- parsing/g_xml.ml4 | 4 -- parsing/tacextend.ml4 | 3 -- parsing/vernacextend.ml4 | 3 -- plugins/subtac/subtac_cases.ml | 110 -------------------------------------- pretyping/cases.ml | 118 ----------------------------------------- pretyping/classops.ml | 9 +--- pretyping/clenv.ml | 5 -- pretyping/coercion.ml | 6 --- pretyping/evarutil.ml | 23 -------- pretyping/evd.ml | 7 +-- pretyping/tacred.ml | 17 ++---- tactics/auto.ml | 26 +-------- tactics/autorewrite.ml | 2 +- tactics/class_tactics.ml4 | 1 - tactics/decl_interp.ml | 5 -- tactics/decl_proof_instr.ml | 20 ------- tactics/dhyp.ml | 11 +--- tactics/eauto.ml4 | 4 -- tactics/equality.ml | 68 ------------------------ tactics/equality.mli | 5 -- toplevel/class.ml | 13 ----- toplevel/classes.ml | 4 -- toplevel/command.ml | 19 ++----- toplevel/coqinit.ml | 8 --- toplevel/coqtop.ml | 1 - 47 files changed, 53 insertions(+), 695 deletions(-) diff --git a/checker/closure.ml b/checker/closure.ml index ccbfbc4c0..591b353db 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -496,9 +496,6 @@ let rec decomp_stack = function | _ -> Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) | _ -> None -let rec decomp_stackn = function - | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s) - | _ -> assert false let array_of_stack s = let rec stackrec = function | [] -> [] @@ -547,8 +544,6 @@ let lift_fconstr k f = if k=0 then f else lft_fconstr k f let lift_fconstr_vect k v = if k=0 then v else Array.map (fun f -> lft_fconstr k f) v -let lift_fconstr_list k l = - if k=0 then l else List.map (fun f -> lft_fconstr k f) l let clos_rel e i = match expand_rel i e with @@ -857,12 +852,6 @@ let get_nth_arg head n stk = (* Beta reduction: look for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) -let get_arg h stk = - let (depth,stk') = strip_update_shift h stk in - match decomp_stack stk' with - Some (v, s') -> (Some (depth,v), s') - | None -> (None, zshift depth stk') - let rec get_args n tys f e stk = match stk with Zupdate r :: s -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9723f2c22..0d2fecfa2 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -92,19 +92,6 @@ let insert_pat_alias loc p = function (**********************************************************************) (* conversion of references *) -let ids_of_ctxt ctxt = - Array.to_list - (Array.map - (function c -> match kind_of_term c with - | Var id -> id - | _ -> - error "Arbitrary substitution of references not implemented.") - ctxt) - -let idopt_of_name = function - | Name id -> Some id - | Anonymous -> None - let extern_evar loc n l = if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None) @@ -574,33 +561,6 @@ let rec rename_rawconstr_var id0 id1 = function | RVar(loc,id) when id=id0 -> RVar(loc,id1) | c -> map_rawconstr (rename_rawconstr_var id0 id1) c -let rec share_fix_binders n rbl ty def = - match ty,def with - RProd(_,na0,bk0,t0,b), RLambda(_,na1,bk1,t1,m) -> - if not(same_rawconstr t0 t1) then List.rev rbl, ty, def - else - let (na,b,m) = - match na0, na1 with - Name id0, Name id1 -> - if id0=id1 then (na0,b,m) - else if not (occur_rawconstr id1 b) then - (na1,rename_rawconstr_var id0 id1 b,m) - else if not (occur_rawconstr id0 m) then - (na1,b,rename_rawconstr_var id1 id0 m) - else (* vraiment pas de chance! *) - failwith "share_fix_binders: capture" - | Name id, Anonymous -> - if not (occur_rawconstr id m) then (na0,b,m) - else - failwith "share_fix_binders: capture" - | Anonymous, Name id -> - if not (occur_rawconstr id b) then (na1,b,m) - else - failwith "share_fix_binders: capture" - | _ -> (na1,b,m) in - share_fix_binders (n-1) ((na,None,t0)::rbl) b m - | _ -> List.rev rbl, ty, def - (**********************************************************************) (* mapping rawterms to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) @@ -910,13 +870,6 @@ let extern_sort s = extern_rawsort (detype_sort s) (******************************************************************) (* Main translation function from pattern -> constr_expr *) -let it_destPLambda n c = - let rec aux n nal c = - if n=0 then (nal,c) else match c with - | PLambda (na,_,c) -> aux (n-1) (na::nal) c - | _ -> anomaly "it_destPLambda" in - aux n [] c - let rec raw_of_pat env = function | PRef ref -> RRef (loc,ref) | PVar id -> RVar (loc,id) @@ -965,9 +918,6 @@ let rec raw_of_pat env = function | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> RSort (loc,s) -and raw_of_eqns env constructs consnargsl bl = - Array.to_list (array_map3 (raw_of_eqn env) constructs consnargsl bl) - and raw_of_eqn env constr construct_nargs branch = let make_pat x env b ids = let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 172d032b5..2aee2ea68 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -113,11 +113,6 @@ let explain_internalisation_error e = | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in pp ++ str "." -let error_unbound_patvar loc n = - user_err_loc - (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ - str " is unbound.") - let error_bad_inductive_type loc = user_err_loc (loc,"",str "This should be an inductive type applied to names or \"_\".") @@ -390,12 +385,6 @@ let apply_scope_env (ids,unb,_,scopes) = function | [] -> (ids,unb,None,scopes), [] | sc::scl -> (ids,unb,sc,scopes), scl -let rec adjust_scopes env scopes = function - | [] -> [] - | a::args -> - let (enva,scopes) = apply_scope_env env scopes in - enva :: adjust_scopes env scopes args - let rec simple_adjust_scopes n = function | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) [] | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes @@ -1210,9 +1199,6 @@ let intern_pattern env patt = user_err_loc (loc,"internalize",explain_internalisation_error e) -let intern_ltac isarity ltacvars sigma env c = - intern_gen isarity sigma env ~ltacvars:ltacvars c - type manual_implicits = (explicitation * (bool * bool * bool)) list (*********************************************************************) @@ -1289,10 +1275,6 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = let interp_type_evars evdref env ?(impls=([],[])) c = interp_constr_evars_gen evdref env IsType ~impls c -let interp_constr_judgment_evars evdref env c = - Default.understand_judgment_tcc evdref env - (intern_constr ( !evdref) env c) - type ltac_sign = identifier list * unbound_ltac_var_map let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index f9881673d..71f38063a 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -154,16 +154,6 @@ let add_glob_kn loc kn = let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in add_glob_gen loc sp lib_dp "syndef" -let add_local loc id = () -(* let mod_dp,id = repr_path sp in *) -(* let mod_dp = remove_sections mod_dp in *) -(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *) -(* let filepath = string_of_dirpath lib_dp in *) -(* let modpath = string_of_dirpath mod_dp_trunc in *) -(* let ident = string_of_id id in *) -(* dump_string (Printf.sprintf "R%d %s %s %s %s\n" *) -(* (fst (unloc loc)) filepath modpath ident ty) *) - let dump_binding loc id = () let dump_definition (loc, id) sec s = diff --git a/kernel/closure.ml b/kernel/closure.ml index 10ef06993..c4759fa92 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -379,9 +379,6 @@ let rec decomp_stack = function | _ -> Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) | _ -> None -let rec decomp_stackn = function - | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s) - | _ -> assert false let array_of_stack s = let rec stackrec = function | [] -> [] @@ -430,8 +427,6 @@ let lift_fconstr k f = if k=0 then f else lft_fconstr k f let lift_fconstr_vect k v = if k=0 then v else Array.map (fun f -> lft_fconstr k f) v -let lift_fconstr_list k l = - if k=0 then l else List.map (fun f -> lft_fconstr k f) l let clos_rel e i = match expand_rel i e with @@ -741,12 +736,6 @@ let get_nth_arg head n stk = (* Beta reduction: look for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) -let get_arg h stk = - let (depth,stk') = strip_update_shift h stk in - match decomp_stack stk' with - Some (v, s') -> (Some (depth,v), s') - | None -> (None, zshift depth stk') - let rec get_args n tys f e stk = match stk with Zupdate r :: s -> diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 58668c014..0851c7a5f 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -45,14 +45,6 @@ let set_strategy k l = else Cmap.add c l !cst_opacity | RelKey _ -> Util.error "set_strategy: RelKey" -let set_transparent_const kn = - cst_opacity := Cmap.remove kn !cst_opacity -let set_transparent_var id = - var_opacity := Idmap.remove id !var_opacity - -let set_opaque_const kn = set_strategy (ConstKey kn) Opaque -let set_opaque_var id = set_strategy (VarKey id) Opaque - let get_transp_state () = (Idmap.fold (fun id l ts -> if l=Opaque then Idpred.remove id ts else ts) diff --git a/kernel/entries.ml b/kernel/entries.ml index 8dde8fb3e..e30fe7737 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -70,14 +70,7 @@ type constant_entry = (*s Modules *) -type specification_entry = - SPEconst of constant_entry - | SPEmind of mutual_inductive_entry - | SPEmodule of module_entry - | SPEalias of module_path - | SPEmodtype of module_struct_entry - -and module_struct_entry = +type module_struct_entry = MSEident of module_path | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry | MSEwith of module_struct_entry * with_declaration @@ -87,8 +80,6 @@ and with_declaration = With_Module of identifier list * module_path | With_Definition of identifier list * constr -and module_structure = (label * specification_entry) list - and module_entry = { mod_entry_type : module_struct_entry option; mod_entry_expr : module_struct_entry option} diff --git a/kernel/entries.mli b/kernel/entries.mli index 6de90d29c..dc1522dbf 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -69,14 +69,7 @@ type constant_entry = (*s Modules *) -type specification_entry = - SPEconst of constant_entry - | SPEmind of mutual_inductive_entry - | SPEmodule of module_entry - | SPEalias of module_path - | SPEmodtype of module_struct_entry - -and module_struct_entry = +type module_struct_entry = MSEident of module_path | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry | MSEwith of module_struct_entry * with_declaration @@ -86,8 +79,6 @@ and with_declaration = With_Module of identifier list * module_path | With_Definition of identifier list * constr -and module_structure = (label * specification_entry) list - and module_entry = { mod_entry_type : module_struct_entry option; mod_entry_expr : module_struct_entry option} diff --git a/kernel/environ.ml b/kernel/environ.ml index 4fb5a2b1a..e0f364f2e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -60,12 +60,6 @@ let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt - -let reset_rel_context env = - { env with - env_rel_context = empty_rel_context; - env_rel_val = []; - env_nb_rel = 0 } let fold_rel_context f env ~init = let rec fold_right env = diff --git a/kernel/names.ml b/kernel/names.ml index 6ee96fddd..953c13aa9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -51,13 +51,7 @@ type name = Name of identifier | Anonymous type module_ident = identifier type dir_path = module_ident list -module ModIdOrdered = - struct - type t = identifier - let compare = Pervasives.compare - end - -module ModIdmap = Map.Make(ModIdOrdered) +module ModIdmap = Idmap let make_dirpath x = x let repr_dirpath x = x diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 44f5dcb32..44d13a0cb 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -77,14 +77,9 @@ type flags = {fastcomputation : bool} (*A definition of maps from strings to pro_int31, to be able to have any amount of coq representation for the 31bits integers *) -module OrderedField = -struct - type t = field - let compare = compare -end - -module Proactive = Map.Make (OrderedField) +module Proactive = + Map.Make (struct type t = field let compare = compare end) type proactive = entry Proactive.t @@ -98,13 +93,8 @@ type proactive = entry Proactive.t a finite type describing the fields to the field of proactive retroknowledge (and then to make as many functions as needed in environ.ml) *) -module OrderedEntry = -struct - type t = entry - let compare = compare -end - -module Reactive = Map.Make (OrderedEntry) +module Reactive = + Map.Make (struct type t = entry let compare = compare end) type reactive_end = {(*information required by the compiler of the VM *) vm_compiling : diff --git a/kernel/univ.ml b/kernel/univ.ml index 65fc78203..24af5da05 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -55,19 +55,17 @@ let cmp_univ_level u v = match u,v with else if i1 > i2 then 1 else compare dp1 dp2 -type universe = - | Atom of universe_level - | Max of universe_level list * universe_level list - -module UniverseOrdered = struct - type t = universe_level - let compare = cmp_univ_level -end - let string_of_univ_level = function | Set -> "0" | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n +module UniverseLMap = + Map.Make (struct type t = universe_level let compare = cmp_univ_level end) + +type universe = + | Atom of universe_level + | Max of universe_level list * universe_level list + let make_univ (m,n) = Atom (Level (m,n)) let pr_uni_level u = str (string_of_univ_level u) @@ -121,18 +119,17 @@ type univ_entry = Canonical of canonical_arc | Equiv of universe_level * universe_level -module UniverseMap = Map.Make(UniverseOrdered) -type universes = univ_entry UniverseMap.t - +type universes = univ_entry UniverseLMap.t + let enter_equiv_arc u v g = - UniverseMap.add u (Equiv(u,v)) g + UniverseLMap.add u (Equiv(u,v)) g let enter_arc ca g = - UniverseMap.add ca.univ (Canonical ca) g + UniverseLMap.add ca.univ (Canonical ca) g let declare_univ u g = - if not (UniverseMap.mem u g) then + if not (UniverseLMap.mem u g) then enter_arc (terminal u) g else g @@ -162,7 +159,7 @@ let is_univ_variable = function let type1_univ = Max ([],[Set]) -let initial_universes = UniverseMap.empty +let initial_universes = UniverseLMap.empty (* Every universe_level has a unique canonical arc representative *) @@ -171,7 +168,7 @@ let initial_universes = UniverseMap.empty let repr g u = let rec repr_rec u = let a = - try UniverseMap.find u g + try UniverseLMap.find u g with Not_found -> anomalylabstrm "Univ.repr" (str"Universe " ++ pr_uni_level u ++ str" undefined") in @@ -443,7 +440,7 @@ let enforce_univ_relation g = function (* Merging 2 universe graphs *) (* let merge_universes sp u1 u2 = - UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2 + UniverseLMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2 *) @@ -571,14 +568,14 @@ let no_upper_constraints u cst = (* Pretty-printing *) let num_universes g = - UniverseMap.fold (fun _ _ -> succ) g 0 + UniverseLMap.fold (fun _ _ -> succ) g 0 let num_edges g = let reln_len = function | Equiv _ -> 1 | Canonical {lt=lt;le=le} -> List.length lt + List.length le in - UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0 + UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0 let pr_arc = function | Canonical {univ=u; lt=[]; le=[]} -> @@ -594,7 +591,7 @@ let pr_arc = function pr_uni_level u ++ str " = " ++ pr_uni_level v ++ fnl () let pr_universes g = - let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in + let graph = UniverseLMap.fold (fun k a l -> (k,a)::l) g [] in prlist (function (_,a) -> pr_arc a) graph let pr_constraints c = @@ -626,7 +623,7 @@ let dump_universes output g = Printf.fprintf output "%s = %s ;\n" (string_of_univ_level u) (string_of_univ_level v) in - UniverseMap.iter dump_arc g + UniverseLMap.iter dump_arc g (* Hash-consing *) diff --git a/lib/bigint.ml b/lib/bigint.ml index a836d0e07..3b974652b 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -167,8 +167,6 @@ let less_than m n = (Array.length m = Array.length n && less_than_same_size m n 0 0)) let equal m n = (m = n) - -let less_or_equal_than m n = equal m n or less_than m n let less_than_shift_pos k m n = (Array.length m - k < Array.length n) @@ -335,9 +333,7 @@ let one = big_of_int 1 let sub_1 n = sub n one let add_1 n = add n one let two = big_of_int 2 -let neg_two = big_of_int (-2) let mult_2 n = add n n -let is_zero n = n=zero let div2_with_rest n = let (q,b) = euclid n two in diff --git a/library/declare.ml b/library/declare.ml index 2a4b2e403..9e242d2b3 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -75,7 +75,7 @@ let discharge_variable (_,o) = match o with | Inr (id,_) -> Some (Inl (variable_constraints id)) | Inl _ -> Some o -let (inVariable, outVariable) = +let (inVariable,_) = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; discharge_function = discharge_variable; @@ -143,7 +143,7 @@ let export_constant cst = Some (dummy_constant cst) let classify_constant (_,cst) = Substitute (dummy_constant cst) -let (inConstant, outConstant) = +let (inConstant,_) = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; @@ -262,7 +262,7 @@ let dummy_inductive_entry (_,m) = ([],{ let export_inductive x = Some (dummy_inductive_entry x) -let (inInductive, outInductive) = +let (inInductive,_) = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; diff --git a/library/declaremods.ml b/library/declaremods.ml index 129ea4ef2..52fa94569 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -114,11 +114,6 @@ let mp_of_kn kn = else anomaly ("Non-empty section in module name!" ^ string_of_kn kn) -let is_bound mp = - match mp with - | MPbound _ -> true - | _ -> false - let dir_of_sp sp = let dir,id = repr_path sp in extend_dirpath dir id @@ -490,7 +485,7 @@ let open_keep i ((sp,kn),seg) = let dirpath,mp = dir_of_sp sp, mp_of_kn kn in open_objects i (dirpath,(mp,empty_dirpath)) seg -let (in_modkeep,out_modkeep) = +let (in_modkeep,_) = declare_object {(default_object "MODULE KEEP OBJECTS") with cache_function = cache_keep; load_function = load_keep; @@ -575,7 +570,7 @@ let classify_modtype (_,(_,substobjs)) = Substitute (None,substobjs) -let (in_modtype,out_modtype) = +let (in_modtype,_) = declare_object {(default_object "MODULE TYPE") with cache_function = cache_modtype; open_function = open_modtype; @@ -859,7 +854,7 @@ let subst_import (_,subst,(export,mp as obj)) = if mp'==mp then obj else (export,mp') -let (in_import,out_import) = +let (in_import,_) = declare_object {(default_object "IMPORT MODULE") with cache_function = cache_import; open_function = (fun i o -> if i=1 then cache_import o); diff --git a/library/decls.ml b/library/decls.ml index 8a67de4ec..5a8729215 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -70,7 +70,3 @@ let last_section_hyps dir = with Not_found -> sec_ids) (Environ.named_context (Global.env())) ~init:[] - -let is_section_variable = function - | VarRef _ -> true - | _ -> false diff --git a/library/goptions.ml b/library/goptions.ml index b614ed34a..b5a8b00ea 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -77,8 +77,7 @@ module MakeTable = if List.mem_assoc nick !A.table then error "Sorry, this table name is already used" - module MyType = struct type t = A.t let compare = Pervasives.compare end - module MySet = Set.Make(MyType) + module MySet = Set.Make (struct type t = A.t let compare = compare end) let t = ref (MySet.empty : MySet.t) @@ -219,8 +218,8 @@ type 'a option_sig = { type option_type = bool * (unit -> value) -> (value -> unit) -module Key = struct type t = option_name let compare = Pervasives.compare end -module OptionMap = Map.Make(Key) +module OptionMap = + Map.Make (struct type t = option_name let compare = compare end) let value_tab = ref OptionMap.empty diff --git a/library/heads.ml b/library/heads.ml index 1b1dba43f..ea3acbbe8 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -39,12 +39,8 @@ type head_approximation = (** Registration as global tables and rollback. *) -module Evalreford = struct - type t = evaluable_global_reference - let compare = Pervasives.compare -end - -module Evalrefmap = Map.Make(Evalreford) +module Evalrefmap = + Map.Make (struct type t = evaluable_global_reference let compare = compare end) let head_map = ref Evalrefmap.empty diff --git a/library/libnames.ml b/library/libnames.ml index f0fcd94c9..44da7b6de 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -66,8 +66,6 @@ module RefOrdered = module Refset = Set.Make(RefOrdered) module Refmap = Map.Make(RefOrdered) -let inductives_table = ref Indmap.empty - (**********************************************) let pr_dirpath sl = (str (string_of_dirpath sl)) diff --git a/library/libobject.mli b/library/libobject.mli index 61e650e6b..d104635cd 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -102,7 +102,7 @@ val ident_subst_function : object_name * substitution * 'a -> 'a type obj -val declare_object : +val declare_object : 'a object_declaration -> ('a -> obj) * (obj -> 'a) val object_tag : obj -> string diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 66fc4c253..8db62c392 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -33,10 +33,6 @@ let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty)) -let mk_lam = function - ([],c) -> c - | (bl,c) -> CLambdaN(constr_loc c, bl,c) - let loc_of_binder_let = function | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc | LocalRawDef ((loc,_),_)::_ -> loc diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ec1e7415b..f656fb32e 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -120,11 +120,6 @@ let test_plurial_form = function "Keywords Variables/Hypotheses/Parameters expect more than one assumption" | _ -> () -let no_coercion loc (c,x) = - if c then Util.user_err_loc - (loc,"no_coercion",str"No coercion allowed here."); - x - (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 3a57fd545..814236835 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -71,10 +71,6 @@ let error_expect_no_argument loc = let nmtoken (loc,a) = try int_of_string a with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") - -let interp_xml_attr_qualid = function - | "uri", s -> qualid_of_string s - | _ -> error "Ill-formed xml attribute" let get_xml_attr s al = try List.assoc s al diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 65b3a075e..03c704758 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -16,9 +16,6 @@ open Q_util open Q_coqast open Argextend -let loc = Util.dummy_loc -let default_loc = <:expr< Util.dummy_loc >> - type grammar_tactic_production_expr = | TacTerm of string | TacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index f661800a1..dd6b9e8bf 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -16,9 +16,6 @@ open Q_util open Q_coqast open Argextend -let loc = Util.dummy_loc -let default_loc = <:expr< Util.dummy_loc >> - type grammar_tactic_production_expr = | VernacTerm of string | VernacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 26507a1ca..1e5722ef1 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -50,9 +50,6 @@ let make_anonymous_patvars = (* Environment management *) let push_rels vars env = List.fold_right push_rel vars env -let push_rel_defs = - List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e) - (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -152,8 +149,6 @@ and pattern_continuation = let start_history n = Continuation (n, [], Top) -let initial_history = function Continuation (_,[],Top) -> true | _ -> false - let feed_history arg = function | Continuation (n, l, h) when n>=1 -> Continuation (n-1, arg :: l, h) @@ -392,9 +387,6 @@ let map_tomatch_type f = function let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) let lift_tomatch_type n = liftn_tomatch_type n 1 -let lift_tomatch n ((current,typ),info) = - ((lift n current,lift_tomatch_type n typ),info) - (**********************************************************************) (* Utilities on patterns *) @@ -407,12 +399,6 @@ let alias_of_pat = function | PatVar (_,name) -> name | PatCstr(_,_,_,name) -> name -let unalias_pat = function - | PatVar (c,name) as p -> - if name = Anonymous then p else PatVar (c,Anonymous) - | PatCstr(a,b,c,name) as p -> - if name = Anonymous then p else PatCstr (a,b,c,Anonymous) - let remove_current_pattern eqn = match eqn.patterns with | pat::pats -> @@ -581,9 +567,6 @@ let replace_tomatch n c = ::(replrec (depth+1) rest) in replrec 0 -let liftn_rel_declaration n k = map_rel_declaration (liftn n k) -let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k) - let rec liftn_tomatch_stack n depth = function | [] -> [] | Pushed ((c,tm),l)::rest -> @@ -1319,99 +1302,6 @@ let matx_of_eqns env eqns = (************************************************************************) (* preparing the elimination predicate if any *) -let build_expected_arity env isevars isdep tomatchl = - let cook n = function - | _,IsInd (_,IndType(indf,_)) -> - let indf' = lift_inductive_family n indf in - Some (build_dependent_inductive env indf', fst (get_arity env indf')) - | _,NotInd _ -> None - in - let rec buildrec n env = function - | [] -> new_Type () - | tm::ltm -> - match cook n tm with - | None -> buildrec n env ltm - | Some (ty1,aritysign) -> - let rec follow n env = function - | d::sign -> - mkProd_or_LetIn_name env - (follow (n+1) (push_rel d env) sign) d - | [] -> - if isdep then - mkProd (Anonymous, ty1, - buildrec (n+1) - (push_rel_assum (Anonymous, ty1) env) - ltm) - else buildrec n env ltm - in follow n env (List.rev aritysign) - in buildrec 0 env tomatchl - -let extract_predicate_conclusion isdep tomatchl pred = - let cook = function - | _,IsInd (_,IndType(_,args)) -> Some (List.length args) - | _,NotInd _ -> None in - let rec decomp_lam_force n l p = - if n=0 then (l,p) else - match kind_of_term p with - | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c - | _ -> (* eta-expansion *) - let na = Name (id_of_string "x") in - decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in - let rec buildrec allnames p = function - | [] -> (List.rev allnames,p) - | tm::ltm -> - match cook tm with - | None -> - let p = - (* adjust to a sign containing the NotInd's *) - if isdep then lift 1 p else p in - let names = if isdep then [Anonymous] else [] in - buildrec (names::allnames) p ltm - | Some n -> - let n = if isdep then n+1 else n in - let names,p = decomp_lam_force n [] p in - buildrec (names::allnames) p ltm - in buildrec [] pred tomatchl - -let set_arity_signature dep n arsign tomatchl pred x = - (* avoid is not exhaustive ! *) - let rec decomp_lam_force n avoid l p = - if n = 0 then (List.rev l,p,avoid) else - match p with - | RLambda (_,(Name id as na),k,_,c) -> - decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c - | _ -> - let x = next_ident_away (id_of_string "x") avoid in - decomp_lam_force (n-1) (x::avoid) (Name x :: l) - (* eta-expansion *) - (let a = RVar (dummy_loc,x) in - match p with - | RApp (loc,p,l) -> RApp (loc,p,l@[a]) - | _ -> (RApp (dummy_loc,p,[a]))) in - let rec decomp_block avoid p = function - | ([], _) -> x := Some p - | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l') -> - let (ind,params) = dest_ind_family indf in - let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p - in - let na,p,avoid' = - if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid' - in - y := - (List.hd na, - if List.for_all ((=) Anonymous) nal then - None - else - Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal)); - decomp_block avoid' p (l,l') - | (_::l),(y::l') -> - y := (Anonymous,None); - decomp_block avoid p (l,l') - | _ -> anomaly "set_arity_signature" - in - decomp_block [] pred (tomatchl,arsign) - let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c = let cook (n, l, env, signs) = function | c,IsInd (_,IndType(indf,realargs)) -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 8451d1285..70b201a6e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -124,9 +124,6 @@ let make_anonymous_patvars n = (* Environment management *) let push_rels vars env = List.fold_right push_rel vars env -let push_rel_defs = - List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e) - (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -210,8 +207,6 @@ and pattern_continuation = let start_history n = Continuation (n, [], Top) -let initial_history = function Continuation (_,[],Top) -> true | _ -> false - let feed_history arg = function | Continuation (n, l, h) when n>=1 -> Continuation (n-1, arg :: l, h) @@ -452,9 +447,6 @@ let map_tomatch_type f = function let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) let lift_tomatch_type n = liftn_tomatch_type n 1 -let lift_tomatch n ((current,typ),info) = - ((lift n current,lift_tomatch_type n typ),info) - (**********************************************************************) (* Utilities on patterns *) @@ -467,12 +459,6 @@ let alias_of_pat = function | PatVar (_,name) -> name | PatCstr(_,_,_,name) -> name -let unalias_pat = function - | PatVar (c,name) as p -> - if name = Anonymous then p else PatVar (c,Anonymous) - | PatCstr(a,b,c,name) as p -> - if name = Anonymous then p else PatCstr (a,b,c,Anonymous) - let remove_current_pattern eqn = match eqn.patterns with | pat::pats -> @@ -658,9 +644,6 @@ let replace_tomatch n c = :: replrec (depth+1) rest in replrec 0 -let liftn_rel_declaration n k = map_rel_declaration (liftn n k) -let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k) - let rec liftn_tomatch_stack n depth = function | [] -> [] | Pushed ((c,tm),l,dep)::rest -> @@ -1283,102 +1266,6 @@ let matx_of_eqns env tomatchl eqns = rhs = rhs } in List.map build_eqn eqns -(************************************************************************) -(* preparing the elimination predicate if any *) - -let build_expected_arity env evdref isdep tomatchl = - let cook n = function - | _,IsInd (_,IndType(indf,_),_) -> - let indf' = lift_inductive_family n indf in - Some (build_dependent_inductive env indf', fst (get_arity env indf')) - | _,NotInd _ -> None - in - let rec buildrec n env = function - | [] -> new_Type () - | tm::ltm -> - match cook n tm with - | None -> buildrec n env ltm - | Some (ty1,aritysign) -> - let rec follow n env = function - | d::sign -> - mkProd_or_LetIn_name env - (follow (n+1) (push_rel d env) sign) d - | [] -> - if isdep then - mkProd (Anonymous, ty1, - buildrec (n+1) - (push_rel_assum (Anonymous, ty1) env) - ltm) - else buildrec n env ltm - in follow n env (List.rev aritysign) - in buildrec 0 env tomatchl - -let extract_predicate_conclusion isdep tomatchl pred = - let cook = function - | _,IsInd (_,IndType(_,args),_) -> Some (List.length args) - | _,NotInd _ -> None in - let rec decomp_lam_force n l p = - if n=0 then (l,p) else - match kind_of_term p with - | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c - | _ -> (* eta-expansion *) - let na = Name (id_of_string "x") in - decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in - let rec buildrec allnames p = function - | [] -> (List.rev allnames,p) - | tm::ltm -> - match cook tm with - | None -> - let p = - (* adjust to a sign containing the NotInd's *) - if isdep then lift 1 p else p in - let names = if isdep then [Anonymous] else [] in - buildrec (names::allnames) p ltm - | Some n -> - let n = if isdep then n+1 else n in - let names,p = decomp_lam_force n [] p in - buildrec (names::allnames) p ltm - in buildrec [] pred tomatchl - -let set_arity_signature dep n arsign tomatchl pred x = - (* avoid is not exhaustive ! *) - let rec decomp_lam_force n avoid l p = - if n = 0 then (List.rev l,p,avoid) else - match p with - | RLambda (_,(Name id as na),_,_,c) -> - decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),_,_,c) -> decomp_lam_force (n-1) avoid (na::l) c - | _ -> - let x = next_ident_away (id_of_string "x") avoid in - decomp_lam_force (n-1) (x::avoid) (Name x :: l) - (* eta-expansion *) - (let a = RVar (dummy_loc,x) in - match p with - | RApp (loc,p,l) -> RApp (loc,p,l@[a]) - | _ -> (RApp (dummy_loc,p,[a]))) in - let rec decomp_block avoid p = function - | ([], _) -> x := Some p - | ((_,IsInd (_,IndType(indf,realargs),_))::l),(y::l') -> - let (ind,params) = dest_ind_family indf in - let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p - in - let na,p,avoid' = - if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid' - in - y := - (List.hd na, - if List.for_all ((=) Anonymous) nal then - None - else - Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal)); - decomp_block avoid' p (l,l') - | (_::l),(y::l') -> - y := (Anonymous,None); - decomp_block avoid p (l,l') - | _ -> anomaly "set_arity_signature" - in - decomp_block [] pred (tomatchl,arsign) - (***************** Building an inversion predicate ************************) (* Let "match t1 in I1 u11..u1n_1 ... tm in Im um1..umn_m with ... end : T" @@ -1754,11 +1641,6 @@ let prepare_predicate_from_arsign_tycon loc env tomatchs sign arsign c = * tycon to make the predicate if it is not closed. *) -let is_dependent_on_rel x t = - match kind_of_term x with - Rel n -> not (noccur_with_meta n n t) - | _ -> false - let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred = match pred with (* No type annotation *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b0554540a..11d6ed093 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -68,8 +68,6 @@ module Bijint = struct (let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v) else b.v in v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = Gmap.add x b.s b.inv } - let replace n x y b = - let v = Array.copy b.v in v.(n) <- (x,y); { b with v = v } let dom b = Gmap.dom b.inv end @@ -138,8 +136,6 @@ let coercion_info coe = Gmap.find coe !coercion_tab let coercion_exists coe = Gmap.mem coe !coercion_tab -let coercion_params coe_info = coe_info.coe_param - (* find_class_type : env -> evar_map -> constr -> cl_typ * int *) let find_class_type env sigma t = @@ -383,7 +379,7 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = discharge_cl clt, n + ps) -let (inCoercion,outCoercion) = +let (inCoercion,_) = declare_object {(default_object "COERCION") with load_function = load_coercion; cache_function = cache_coercion; @@ -395,9 +391,6 @@ let (inCoercion,outCoercion) = let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps = Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps)) -let coercion_strength v = v.coe_strength -let coercion_identity v = v.coe_is_identity - (* For printing purpose *) let get_coercion_value v = v.coe_value diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 69b5db5e6..576e217aa 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -32,7 +32,6 @@ open Coercion.Default let pf_env gls = Global.env_of_context gls.it.evar_hyps let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c -let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c let pf_concl gl = gl.it.evar_concl (******************************************************************) @@ -167,8 +166,6 @@ let mentions clenv mv0 = meta_exists menrec mlist in menrec -let clenv_defined clenv mv = meta_defined clenv.evd mv - let error_incompatible_inst clenv mv = let na = meta_name clenv.evd mv in match na with @@ -197,8 +194,6 @@ let clenv_assign mv rhs clenv = error "clenv_assign: undefined meta" -let clenv_wtactic f clenv = {clenv with evd = f clenv.evd } - (* [clenv_dependent hyps_only clenv] * returns a list of the metavars which appear in the template of clenv, diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3a5f35125..f8545fdc9 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -73,11 +73,6 @@ module Default = struct (* Typing operations dealing with coercions *) exception NoCoercion - let whd_app_evar sigma t = - match kind_of_term t with - | App (f,l) -> mkApp (whd_evar sigma f,l) - | _ -> whd_evar sigma t - (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function @@ -156,7 +151,6 @@ module Default = struct inh_tosort_force loc env evd j let inh_coerce_to_base loc env evd j = (evd, j) - let inh_coerce_to_prod loc env evd t = (evd, t) let inh_coerce_to_fail env evd rigidonly v t c1 = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d455ec6fe..1a7bb2c6c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -261,10 +261,6 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty = * operations on the evar constraints * *------------------------------------*) -let is_pattern inst = - array_for_all (fun a -> isRel a || isVar a) inst && - array_distinct inst - (* Pb: defined Rels and Vars should not be considered as a pattern... *) (* let is_pattern inst = @@ -275,19 +271,6 @@ let is_pattern inst = is_hopat [] (Array.to_list inst) *) -let evar_well_typed_body evd ev evi body = - try - let env = evar_unfiltered_env evi in - let ty = evi.evar_concl in - Typing.check env ( evd) body ty; - true - with e -> - pperrnl - (str "Ill-typed evar instantiation: " ++ fnl() ++ - pr_evar_defs evd ++ fnl() ++ - str "----> " ++ int ev ++ str " := " ++ - print_constr body); - false (* We have x1..xq |- ?e1 and had to solve something like * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some @@ -807,12 +790,6 @@ let solve_evar_evar f env evd ev1 ev2 = with CannotProject projs2 -> postpone_evar_evar env evd projs1 ev1 projs2 ev2 -let expand_rhs env sigma subst rhs = - let d = (named_hd env rhs Anonymous,Some rhs,get_type_of env sigma rhs) in - let rhs' = lift 1 rhs in - let f (id,(idc,t)) = (id,(idc,replace_term rhs' (mkRel 1) (lift 1 t))) in - push_rel d env, List.map f subst, mkRel 1 - (* We try to instantiate the evar assuming the body won't depend * on arguments that are not Rels or Vars, or appearing several times * (i.e. we tackle a generalization of Miller-Pfenning patterns unification) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0f2f4655b..500e19002 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -177,11 +177,8 @@ type sort_constraint = | SortVar of sort_var list * sort_var list (* (leq,geq) *) | EqSort of sort_var -module UniverseOrdered = struct - type t = Univ.universe - let compare = Pervasives.compare -end -module UniverseMap = Map.Make(UniverseOrdered) +module UniverseMap = + Map.Make (struct type t = Univ.universe let compare = compare end) type sort_constraints = sort_constraint UniverseMap.t diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index d3bbce9e3..55df4b185 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -109,19 +109,12 @@ type constant_evaluation = (* We use a cache registered as a global table *) -module CstOrdered = - struct - type t = constant - let compare = Pervasives.compare - end -module Cstmap = Map.Make(CstOrdered) +let eval_table = ref Cmap.empty -let eval_table = ref Cstmap.empty - -type frozen = (int * constant_evaluation) Cstmap.t +type frozen = (int * constant_evaluation) Cmap.t let init () = - eval_table := Cstmap.empty + eval_table := Cmap.empty let freeze () = !eval_table @@ -272,10 +265,10 @@ let compute_consteval sigma env ref = let reference_eval sigma env = function | EvalConst cst as ref -> (try - Cstmap.find cst !eval_table + Cmap.find cst !eval_table with Not_found -> begin let v = compute_consteval sigma env ref in - eval_table := Cstmap.add cst v !eval_table; + eval_table := Cmap.add cst v !eval_table; v end) | ref -> compute_consteval sigma env ref diff --git a/tactics/auto.ml b/tactics/auto.ml index e7137787b..907995c54 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -61,8 +61,6 @@ type pri_auto_tactic = { type hint_entry = global_reference option * pri_auto_tactic -let pri_ord {pri=pri1} {pri=pri2} = pri1 - pri2 - let pri_order {pri=pri1} {pri=pri2} = pri1 <= pri2 let insert v l = @@ -116,19 +114,6 @@ let is_transparent_gr (ids, csts) = function | VarRef id -> Idpred.mem id ids | ConstRef cst -> Cpred.mem cst csts | IndRef _ | ConstructRef _ -> false - -let fmt_autotactic = - function - | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c) - | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c) - | Give_exact c -> (str"exact " ++ pr_lconstr c) - | Res_pf_THEN_trivial_fail (c,clenv) -> - (str"apply " ++ pr_lconstr c ++ str" ; trivial") - | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) - | Extern tac -> - (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) - -let pr_autotactic = fmt_autotactic module Hint_db = struct @@ -467,7 +452,7 @@ let classify_autohint (_,((local,name,hintlist) as obj)) = let export_autohint ((local,name,hintlist) as obj) = if local then None else Some obj -let (inAutoHint,outAutoHint) = +let (inAutoHint,_) = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; load_function = (fun _ -> cache_autohint); @@ -714,9 +699,6 @@ let print_searchtable () = let priority l = List.filter (fun (_,hint) -> hint.pri = 0) l -let select_unfold_extern = - List.filter (function (_,{code = (Unfold_nth _ | Extern _)}) -> true | _ -> false) - (* tell auto not to reuse already instantiated metas in unification (for compatibility, since otherwise, apply succeeds oftener) *) @@ -1081,10 +1063,6 @@ type autoArguments = | UsingTDB | Destructing -let keepAfter tac1 tac2 = - (tclTHEN tac1 - (function g -> tac2 [pf_last_hyp g] g)) - let compileAutoArg contac = function | Destructing -> (function g -> @@ -1139,8 +1117,6 @@ let search_superauto n to_add argl g = let superauto n to_add argl = tclTRY (tclCOMPLETE (search_superauto n to_add argl)) -let default_superauto g = superauto !default_search_depth [] [] g - let interp_to_add gl r = let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in let id = id_of_global r in diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 68c61bca0..f916e0a3e 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -214,7 +214,7 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x (* Declaration of the Hint Rewrite library object *) -let (inHintRewrite,outHintRewrite)= +let (inHintRewrite,_)= Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with Libobject.cache_function = cache_hintrewrite; Libobject.load_function = (fun _ -> cache_hintrewrite); diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index c28f214c7..31ffc8897 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -60,7 +60,6 @@ let e_give_exact flags c gl = else exact_check c gl (* let t1 = (pf_type_of gl c) in *) (* tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl *) - let assumption flags id = e_give_exact flags (mkVar id) open Unification diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index 2701566ed..02dace837 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -182,11 +182,6 @@ let interp_constr_or_thesis check_sort sigma env = function Thesis n -> Thesis n | This c -> This (interp_constr check_sort sigma env c) -let type_tester_var body typ = - raw_app(dummy_loc, - RLambda(dummy_loc,Anonymous,Explicit,typ, - RSort (dummy_loc,RProp Null)),body) - let abstract_one_hyp inject h raw = match h with Hvar (loc,(id,None)) -> diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 967bc88e8..ef2f77069 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -487,9 +487,6 @@ let thus_tac c ctyp submetas gls = (* general forward step *) - -let anon_id_base = id_of_string "__" - let mk_stat_or_thesis info gls = function This c -> c | Thesis (For _ ) -> @@ -843,12 +840,6 @@ let rec constr_trees (main_ind,wft) ind = constr_trees (None,itree) ind | _,constrs -> main_ind,constrs -let constr_args rp constr = - let main_ind,constrs = constr_trees rp (fst constr) in - let ctree = constrs.(pred (snd constr)) in - array_map_to_list (fun t -> main_ind,t) - (snd (Rtree.dest_node ctree)) - let ind_args rp ind = let main_ind,constrs = constr_trees rp ind in let args ctree = @@ -1212,8 +1203,6 @@ let pop_one (id,stack) = let pop_stacks stacks = List.map pop_one stacks -let patvar_base = id_of_string "__" - let hrec_for fix_id per_info gls obj_id = let obj=mkVar obj_id in let typ=pf_get_hyp_typ gls obj_id in @@ -1392,15 +1381,6 @@ let end_tac et2 gls = (* escape *) -let rec abstract_metas n avoid head = function - [] -> 1,head,[] - | (meta,typ)::rest -> - let id = next_ident_away (id_of_string "_sbgl") avoid in - let p,term,args = abstract_metas (succ n) (id::avoid) head rest in - succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term), - (mkMeta n)::args - - let escape_tac gls = tcl_erase_info gls (* General instruction engine *) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 35d2e1324..b37212d9d 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -175,10 +175,6 @@ let init () = Nbtermdn.empty tactab let freeze () = Nbtermdn.freeze tactab let unfreeze fs = Nbtermdn.unfreeze fs tactab -let rollback f x = - let fs = freeze() in - try f x with e -> (unfreeze fs; raise e) - let add (na,dd) = let pat = match dd.d_pat with | HypLocation(_,p,_) -> p.d_typ @@ -202,8 +198,6 @@ let _ = let forward_subst_tactic = ref (fun _ -> failwith "subst_tactic is not installed for DHyp") -let set_extern_subst_tactic f = forward_subst_tactic := f - let cache_dd (_,(_,na,dd)) = try add (na,dd) @@ -223,7 +217,7 @@ let subst_dd (_,subst,(local,na,dd)) = d_pri = dd.d_pri; d_code = !forward_subst_tactic subst dd.d_code }) -let (inDD,outDD) = +let (inDD,_) = declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with cache_function = cache_dd; open_function = (fun i o -> if i=1 then cache_dd o); @@ -330,7 +324,6 @@ let destructHyp discard id gls = let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls -let cDHyp id gls = destructHyp true id gls let dHyp id gls = destructHyp false id gls let h_destructHyp b id = @@ -349,8 +342,6 @@ let dConcl gls = let h_destructConcl = abstract_tactic TacDestructConcl dConcl -let to2Lists (table : t) = Nbtermdn.to2lists table - let rec search n = if n=0 then error "Search has reached zero."; tclFIRST diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 5e4f847fa..09fc808c6 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -207,8 +207,6 @@ let e_possible_resolve mod_delta db_list local_db gl = (fst (head_constr_bound gl)) gl) with Bound | Not_found -> [] -let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id)) - let find_first_goal gls = try first_goal gls with UserError _ -> assert false @@ -324,8 +322,6 @@ let make_initial_state n gl dblist localdb = dblist = dblist; localdb = [localdb] } -let debug_depth_first = Search.debug_depth_first - let e_depth_search debug p db_list local_db gl = try let tac = if debug then Search.debug_depth_first else Search.depth_first in diff --git a/tactics/equality.ml b/tactics/equality.ml index 99767afc0..99216a127 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -84,11 +84,6 @@ let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause let is_applied_setoid_relation = ref (fun _ -> false) let register_is_applied_setoid_relation = (:=) is_applied_setoid_relation -let is_applied_relation t = - match kind_of_term t with - | App (c, args) when Array.length args >= 2 -> true - | _ -> false - (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) @@ -230,24 +225,14 @@ let conditional_rewrite lft2rgt tac (c,bl) = (general_rewrite_ebindings lft2rgt all_occurrences (c,bl) false) [|tclIDTAC|] (tclCOMPLETE tac) -let rewriteLR_bindings = general_rewrite_bindings true all_occurrences -let rewriteRL_bindings = general_rewrite_bindings false all_occurrences - let rewriteLR = general_rewrite true all_occurrences let rewriteRL = general_rewrite false all_occurrences -let rewriteLRin_bindings = general_rewrite_bindings_in true all_occurrences -let rewriteRLin_bindings = general_rewrite_bindings_in false all_occurrences - let conditional_rewrite_in lft2rgt id tac (c,bl) = tclTHENSFIRSTn (general_rewrite_ebindings_in lft2rgt all_occurrences id (c,bl) false) [|tclIDTAC|] (tclCOMPLETE tac) -let rewriteRL_clause = function - | None -> rewriteRL_bindings - | Some id -> rewriteRLin_bindings id - (* Replacing tactics *) (* eq,sym_eq : equality on Type and its symmetry theorem @@ -973,10 +958,6 @@ let dEqThen with_evars ntac = function let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC) -let rewrite_msg = function - | None -> str "passed term is not a primitive equality" - | Some id -> pr_id id ++ str "does not satisfy preconditions " - let swap_equands gls eqn = let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in applist(lbeq.eq,[t;e2;e1]) @@ -986,10 +967,6 @@ let swapEquandsInConcl gls = let sym_equal = lbeq.sym in refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls -let swapEquandsInHyp id gls = - cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id)) - (tclTHEN swapEquandsInConcl) gls - (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *) let bareRevSubstInConcl lbeq body (t,e1,e2) gls = @@ -1278,49 +1255,4 @@ let replace_multi_term dir_opt c = in rewrite_multi_assumption_cond cond_eq_fun -(* JF. old version -let rewrite_assumption_cond faildir gl = - let rec arec = function - | [] -> error "No such assumption." - | (id,_,t)::rest -> - (try let dir = faildir t gl in - general_rewrite dir (mkVar id) gl - with Failure _ | UserError _ -> arec rest) - in arec (pf_hyps gl) - - -let rewrite_assumption_cond_in faildir hyp gl = - let rec arec = function - | [] -> error "No such assumption." - | (id,_,t)::rest -> - (try let dir = faildir t gl in - general_rewrite_in dir hyp (mkVar id) gl - with Failure _ | UserError _ -> arec rest) - in arec (pf_hyps gl) - -let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t) - -let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t) - -let replace_term t = rewrite_assumption_cond (cond_eq_term t) - -let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t) - -let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t) - -let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t) -*) - -let replace_term_left t = replace_multi_term (Some true) t Tacticals.onConcl - -let replace_term_right t = replace_multi_term (Some false) t Tacticals.onConcl - -let replace_term t = replace_multi_term None t Tacticals.onConcl - -let replace_term_in_left t hyp = replace_multi_term (Some true) t (Tacticals.onHyp hyp) - -let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.onHyp hyp) - -let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp) - let _ = Tactics.register_general_multi_rewrite general_multi_rewrite diff --git a/tactics/equality.mli b/tactics/equality.mli index df59867bb..bcbe3e222 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -32,11 +32,6 @@ val general_rewrite_bindings : val general_rewrite : bool -> occurrences -> constr -> tactic -(* Obsolete, use [general_rewrite_bindings l2r] -[val rewriteLR_bindings : constr with_bindings -> tactic] -[val rewriteRL_bindings : constr with_bindings -> tactic] -*) - (* Equivalent to [general_rewrite l2r] *) val rewriteLR : constr -> tactic val rewriteRL : constr -> tactic diff --git a/toplevel/class.ml b/toplevel/class.ml index d2d399f10..11c5bf398 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -29,10 +29,6 @@ open Safe_typing let strength_min l = if List.mem Local l then Local else Global -let id_of_varid c = match kind_of_term c with - | Var id -> id - | _ -> anomaly "class__id_of_varid" - (* Errors *) type coercion_error_kind = @@ -103,15 +99,6 @@ let uniform_cond nargs lt = in aux (nargs,lt) -let id_of_cl = function - | CL_FUN -> id_of_string "FUNCLASS" - | CL_SORT -> id_of_string "SORTCLASS" - | CL_CONST kn -> id_of_label (con_label kn) - | CL_IND ind -> - let (_,mip) = Global.lookup_inductive ind in - mip.mind_typename - | CL_SECVAR id -> id - let class_of_global = function | ConstRef sp -> CL_CONST sp | IndRef sp -> CL_IND sp diff --git a/toplevel/classes.ml b/toplevel/classes.ml index b6c664020..e5c3322a3 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -37,10 +37,6 @@ let typeclasses_db = "typeclass_instances" let qualid_of_con c = Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c)) -let set_rigid c = - Auto.add_hints false [typeclasses_db] - (Vernacexpr.HintsTransparency ([qualid_of_con c], false)) - let _ = Typeclasses.register_add_instance_hint (fun inst pri -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 6e000bc74..d07c4973e 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -47,9 +47,6 @@ open Mod_subst open Evd open Decls -let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b)) -let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b)) - let rec abstract_constr_expr c = function | [] -> c | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) @@ -73,14 +70,6 @@ let rec under_binders env f n c = mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c) | _ -> assert false -let rec destSubCast c = match kind_of_term c with - | Lambda (x,t,c) -> - let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u) - | LetIn (x,b,t,c) -> - let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u) - | Cast (b,_, u) -> (b,u) - | _ -> assert false - let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) @@ -288,7 +277,7 @@ let _ = optwrite = (fun b -> eq_flag := b) } (* boolean equality *) -let (inScheme,outScheme) = +let (inScheme,_) = declare_object {(default_object "EQSCHEME") with cache_function = Ind_tables.cache_scheme; load_function = (fun _ -> Ind_tables.cache_scheme); @@ -321,21 +310,21 @@ let declare_eq_scheme sp = (* decidability of eq *) -let (inBoolLeib,outBoolLeib) = +let (inBoolLeib,_) = declare_object {(default_object "BOOLLIEB") with cache_function = Ind_tables.cache_bl; load_function = (fun _ -> Ind_tables.cache_bl); subst_function = Auto_ind_decl.subst_in_constr; export_function = Ind_tables.export_bool_leib } -let (inLeibBool,outLeibBool) = +let (inLeibBool,_) = declare_object {(default_object "LIEBBOOL") with cache_function = Ind_tables.cache_lb; load_function = (fun _ -> Ind_tables.cache_lb); subst_function = Auto_ind_decl.subst_in_constr; export_function = Ind_tables.export_leib_bool } -let (inDec,outDec) = +let (inDec,_) = declare_object {(default_object "EQDEC") with cache_function = Ind_tables.cache_dec; load_function = (fun _ -> Ind_tables.cache_dec); diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e736fc676..729db2d02 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -51,9 +51,6 @@ let load_rcfile() = else Flags.if_verbose msgnl (str"Skipping rcfile loading.") -let add_ml_include s = - Mltop.add_ml_dir s - (* Puts dir in the path of ML and in the LoadPath *) let coq_add_path d s = Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s]) @@ -64,11 +61,6 @@ let includes = ref [] let push_include (s, alias) = includes := (s,alias,false) :: !includes let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes -(* Because find puts "./" and the loadpath is not nicely pretty-printed *) -let hm2 s = - let n = String.length s in - if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s - (* The list of all theories in the standard library /!\ order does matter *) let theories_dirs_map = [ "theories/Unicode", "Unicode" ; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cd13c6c88..da63382bf 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -72,7 +72,6 @@ let set_outputstate s = outputstate:=s let outputstate () = if !outputstate <> "" then extern_state !outputstate let set_default_include d = push_include (d,Nameops.default_root_prefix) -let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix) let set_include d p = let p = dirpath_of_string p in Library.check_coq_overwriting p; -- cgit v1.2.3