From 90d64647d3fd5dbf5c337944dc0038f0b19b8a51 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Jun 2014 14:26:02 +0200 Subject: Removing dead code. --- interp/constrintern.ml | 23 ----- interp/coqlib.ml | 10 -- interp/notation.ml | 12 --- interp/syntax_def.ml | 1 - kernel/constr.ml | 6 +- kernel/environ.ml | 6 -- kernel/fast_typeops.ml | 53 ---------- kernel/indtypes.ml | 28 +----- kernel/inductive.ml | 7 -- kernel/reduction.ml | 3 - kernel/safe_typing.ml | 6 -- kernel/term_typing.ml | 13 --- library/heads.ml | 14 --- library/impargs.ml | 1 - library/lib.ml | 4 - library/universes.ml | 44 +-------- plugins/cc/ccproof.ml | 1 - plugins/cc/cctac.ml | 2 - plugins/firstorder/instances.ml | 1 - plugins/funind/functional_principles_types.ml | 17 ---- plugins/funind/recdef.ml | 2 - pretyping/evarconv.ml | 4 +- pretyping/evarsolve.ml | 4 - pretyping/evarutil.ml | 33 ------- pretyping/evd.ml | 52 ---------- pretyping/inductiveops.ml | 1 - pretyping/namegen.ml | 1 - pretyping/pretyping.ml | 10 -- pretyping/recordops.ml | 10 -- pretyping/reductionops.ml | 11 --- pretyping/retyping.ml | 1 - pretyping/tacred.ml | 5 - pretyping/termops.ml | 7 -- printing/ppvernac.ml | 5 - printing/printer.ml | 2 - proofs/tacmach.ml | 2 - stm/stm.ml | 15 +-- tactics/auto.ml | 15 --- tactics/coretactics.ml4 | 3 - tactics/eauto.ml4 | 2 +- tactics/elimschemes.ml | 1 - tactics/eqdecide.ml | 2 - tactics/extraargs.ml4 | 3 - tactics/hipattern.ml4 | 11 --- tactics/rewrite.ml | 135 -------------------------- tactics/tacintern.ml | 4 - tactics/tacinterp.ml | 13 --- tactics/tacsubst.ml | 1 - tactics/tacticals.mli | 2 + tactics/tauto.ml4 | 1 - tactics/term_dnet.ml | 4 +- toplevel/command.ml | 11 --- toplevel/vernac.ml | 2 +- 53 files changed, 12 insertions(+), 615 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 841a89584..93feb8b46 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -28,7 +28,6 @@ open Topconstr open Nametab open Notation open Inductiveops -open Misctypes open Decl_kinds (** constr_expr -> glob_constr translation: @@ -298,12 +297,6 @@ let set_type_scope env = {env with tmp_scope = Some Notation.type_scope} let reset_tmp_scope env = {env with tmp_scope = None} -let set_scope env = function - | CastConv (GSort _) -> set_type_scope env - | CastConv (GRef (_,ref,_) | GApp (_,GRef (_,ref,_),_)) -> - {env with tmp_scope = compute_scope_of_global ref} - | _ -> env - let rec it_mkGProd loc2 env body = match env with (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body)) @@ -1299,18 +1292,6 @@ let merge_impargs l args = | _ -> a::l) l args -let check_projection isproj nargs r = - match (r,isproj) with - | GRef (loc, ref, _), Some _ -> - (try - if not (Int.equal nargs 1) then - user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters."); - with Not_found -> - user_err_loc - (loc,"",pr_global_env Id.Set.empty ref ++ str " is not a registered projection.")) - | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.") - | _, None -> () - let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) @@ -1360,10 +1341,6 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let is_projection_ref env = function - | ConstRef c -> Environ.is_projection c env - | _ -> false - let internalize globalenv env allow_patvar lvar c = let rec intern env = function | CRef (ref,us) as x -> diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 3df071aff..6c4d76340 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -99,10 +99,6 @@ let init_constant dir s = let d = "Init"::dir in check_required_library (coq::d); gen_constant "Coqlib" d s -let logic_constant dir s = - let d = "Logic"::dir in - check_required_library (coq::d); gen_constant "Coqlib" d s - let logic_reference dir s = let d = "Logic"::dir in check_required_library ("Coq"::d); gen_reference "Coqlib" d s @@ -139,9 +135,6 @@ let logic_type_module = make_dir logic_type_module_name let datatypes_module_name = init_dir@["Datatypes"] let datatypes_module = make_dir datatypes_module_name -let arith_module_name = arith_dir@["Arith"] -let arith_module = make_dir arith_module_name - let jmeq_module_name = [coq;"Logic";"JMeq"] let jmeq_module = make_dir jmeq_module_name @@ -273,9 +266,6 @@ let build_coq_eq_data () = trans = Lazy.force coq_eq_trans; congr = Lazy.force coq_eq_congr } -let make_dirpath dir = - Names.make_dirpath (List.map id_of_string dir) - let build_coq_eq () = Lazy.force coq_eq_eq let build_coq_eq_refl () = Lazy.force coq_eq_refl let build_coq_eq_sym () = Lazy.force coq_eq_sym diff --git a/interp/notation.ml b/interp/notation.ml index 6fd6001f4..ec82c8aea 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -214,18 +214,6 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of kernel_name -let compare_interp_rule x y = - match x, y with - | NotationRule (sno1, n1), NotationRule (sno2, n2) -> - (match sno1, sno2 with - | None, None -> String.compare n1 n2 - | None, Some _ -> -1 - | Some sn1, Some sn2 -> String.compare sn1 sn2 - | Some _, None -> 1) - | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2 - | NotationRule _, SynDefRule _ -> -1 - | SynDefRule _, NotationRule _ -> 1 - (* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index a023462b7..524f6d743 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -82,7 +82,6 @@ let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let pr_global r = pr_global_env Id.Set.empty r let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) let allow_compat_notations = ref true diff --git a/kernel/constr.ml b/kernel/constr.ml index 9be04c765..b2aa5690b 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -143,7 +143,6 @@ let mkApp (f, a) = | App (g, cl) -> App (g, Array.append cl a) | _ -> App (f, a) -let out_punivs (a, _) = a let map_puniverses f (x,u) = (f x, u) let in_punivs a = (a, Univ.Instance.empty) @@ -547,9 +546,6 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 = let rec eq_constr m n = (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n -(** Strict equality of universe instances. *) -let compare_constr = compare_head_gen (fun _ -> Instance.equal) Sorts.equal - let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = @@ -989,7 +985,7 @@ module Hsorts = | Type u -> 2 + Universe.hash u end) -let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ +(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *) let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind let hcons = diff --git a/kernel/environ.ml b/kernel/environ.ml index 5bd0edf69..48a7964c3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -220,10 +220,6 @@ let universes_and_subst_of cb u = let subst = Univ.make_universe_subst u univs in subst, Univ.instantiate_univ_context subst univs -let get_regular_arity = function - | RegularArity a -> a - | TemplateArity _ -> assert false - let map_regular_arity f = function | RegularArity a as ar -> let a' = f a in @@ -374,8 +370,6 @@ let add_mind kn mib env = (* Lookup of section variables *) -let constant_body_hyps cb = cb.const_hyps - let lookup_constant_variables c env = let cmap = lookup_constant c env in Context.vars_of_named_context cmap.const_hyps diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 94e4479d2..83f1e74ba 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -12,10 +12,8 @@ open Names open Univ open Term open Vars -open Context open Declarations open Environ -open Entries open Reduction open Inductive open Type_errors @@ -62,7 +60,6 @@ let assumption_of_judgment env t ty = (* Prop and Set *) let judge_of_prop = mkSort type1_sort -let judge_of_set = judge_of_prop let judge_of_prop_contents _ = judge_of_prop @@ -122,16 +119,6 @@ let type_of_constant_knowing_parameters env cst paramtyps = let ty, cu = constant_type env cst in type_of_constant_knowing_parameters_arity env ty paramtyps, cu -let type_of_constant_type env t = - type_of_constant_knowing_parameters_arity env t [||] - -let type_of_constant env cst = - type_of_constant_knowing_parameters env cst [||] - -let type_of_constant_in env cst = - let ar = constant_type_in env cst in - type_of_constant_knowing_parameters_arity env ar [||] - let judge_of_constant_knowing_parameters env (kn,u as cst) args = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in @@ -142,18 +129,6 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) args = let judge_of_constant env cst = judge_of_constant_knowing_parameters env cst [||] -let type_of_projection env (cst,u) = - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if cb.const_polymorphic then - let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in - let subst = make_inductive_subst mib u in - Vars.subst_univs_level_constr subst pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") - - (* Type of a lambda-abstraction. *) (* [judge_of_abstraction env name var j] implements the rule @@ -169,11 +144,6 @@ let type_of_projection env (cst,u) = let judge_of_abstraction env name var ty = mkProd (name, var, ty) -(* Type of let-in. *) - -let judge_of_letin env name defj typj j = - subst1 defj j - (* Type of an application. *) let make_judgev c t = @@ -490,26 +460,3 @@ let infer_type env constr = let infer_v env cv = let jv = execute_array env cv in make_judgev cv jv - -(* Typing of several terms. *) - -let infer_local_decl env id = function - | LocalDef c -> - let t = execute env c in - (Name id, Some c, t) - | LocalAssum c -> - let t = execute env c in - (Name id, None, assumption_of_judgment env c t) - -let infer_local_decls env decls = - let rec inferec env = function - | (id, d) :: l -> - let (env, l) = inferec env l in - let d = infer_local_decl env id d in - (push_rel d env, add_rel_decl d l) - | [] -> (env, empty_rel_context) in - inferec env decls - -(* Exported typing functions *) - -let typing env c = infer env c diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 85d04e5e2..014bfba29 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -102,14 +102,6 @@ let mind_check_names mie = (* Typing the arities and constructor types *) -let is_logic_type t = is_prop_sort t.utj_type - -(* [infos] is a sequence of pair [islogic,issmall] for each type in - the product of a constructor or arity *) - -let is_small infos = List.for_all (fun (logic,small) -> small) infos -let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos - (* An inductive definition is a "unit" if it has only one constructor and that all arguments expected by this constructor are logical, this is the case for equality, conjunction of logical properties @@ -153,23 +145,9 @@ let infos_and_sort env ctx t = w1,w2,w3 <= u3 *) -let extract_level (_,_,lc,(_,lev)) = - (* Enforce that the level is not in Prop if more than one constructor *) - (* if Array.length lc >= 2 then sup type0_univ lev else lev *) - lev - -let inductive_levels arities inds = - let cstrs_levels = Array.map extract_level inds in - (* Take the transitive closure of the system of constructors *) - (* level constraints and remove the recursive dependencies *) - cstrs_levels - (* This (re)computes informations relevant to extraction and the sort of an arity or type constructor; we do not to recompute universes constraints *) -let context_set_list_union = - List.fold_left ContextSet.union ContextSet.empty - let infer_constructor_packet env_ar_par ctx params lc = (* type-check the constructors *) let jlc = List.map (infer_type env_ar_par) lc in @@ -691,11 +669,7 @@ let used_section_variables env inds = Id.Set.empty inds in keep_hyps env ids -let lift_decl n d = - map_rel_declaration (lift n) d - let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) -let rel_list n m = Array.to_list (rel_vect n m) let rel_appvect n m = rel_vect n (List.length m) exception UndefinableExpansion @@ -707,7 +681,7 @@ exception UndefinableExpansion let compute_expansion ((kn, _ as ind), u) params ctx = let mp, dp, l = repr_mind kn in let make_proj id = Constant.make1 (KerName.make mp dp (Label.of_id id)) in - let rec projections acc (na, b, t) = + let projections acc (na, b, t) = match b with | Some c -> acc | None -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f07217ac0..64b2c76f9 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -19,9 +19,6 @@ open Environ open Reduction open Type_errors -type pinductive = inductive puniverses -type pconstructor = constructor puniverses - type mind_specif = mutual_inductive_body * one_inductive_body (* raise Not_found if not an inductive type *) @@ -157,10 +154,6 @@ let sort_as_univ = function let cons_subst u su subst = Univ.LMap.add u su subst -let actualize_decl_level env lev t = - let sign,s = dest_arity env t in - mkArity (sign,lev) - (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) let rec make_subst env = function diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a6e107d3f..1e6f157ab 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -172,7 +172,6 @@ type conv_pb = | CUMUL let is_cumul = function CUMUL -> true | CONV -> false -let is_pos = function Pos -> true | Null -> false type 'a universe_compare = { (* Might raise NotConvertible *) @@ -186,8 +185,6 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints -type conv_universes = Univ.universes * Univ.constraints option - let sort_cmp_universes pb s0 s1 (u, check) = (check.compare pb s0 s1 u, check) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 3e11ede0e..0578d35fc 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -802,12 +802,6 @@ let register field value by_clause senv = Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge } -(* spiwack : currently unused *) -let unregister field senv = - (*spiwack: todo: do things properly or delete *) - { senv with env = Environ.unregister senv.env field} -(* /spiwack *) - (* This function serves only for inlining constants in native compiler for now, but it is meant to become a replacement for environ.register *) let register_inline kn senv = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 147fe8a9d..437f7b832 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,10 +24,6 @@ open Entries open Typeops open Fast_typeops -let debug = true -let prerr_endline = - if debug then prerr_endline else fun _ -> () - let constrain_type env j poly = function | `None -> if not poly then (* Old-style polymorphism *) @@ -46,15 +42,6 @@ let constrain_type env j poly = function let map_option_typ = function None -> `None | Some x -> `Some x -let local_constrain_type env j = function - | None -> - j.uj_type - | Some t -> - let tj = infer_type env t in - let _ = judge_of_cast env j DEFAULTcast tj in - assert (eq_constr t tj.utj_val); - t - (* Insertion of constants and parameters in environment. *) let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff diff --git a/library/heads.ml b/library/heads.ml index fa0393019..31908816b 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util open Names open Term @@ -14,7 +13,6 @@ open Vars open Mod_subst open Environ open Globnames -open Nameops open Libobject open Lib @@ -186,15 +184,3 @@ let inHead : head_obj -> obj = let declare_head c = let hd = compute_head c in add_anonymous_leaf (inHead (c,hd)) - -(** Printing *) - -let pr_head = function -| RigidHead (RigidParameter cst) -> str "rigid constant " ++ pr_con cst -| RigidHead (RigidType) -> str "rigid type" -| RigidHead (RigidVar id) -> str "rigid variable " ++ pr_id id -| ConstructorHead -> str "constructor" -| FlexibleHead (k,n,p,b) -> int n ++ str "th of " ++ int k ++ str " binders applied to " ++ int p ++ str " arguments" ++ (if b then str " (with case)" else mt()) -| NotImmediatelyComputableHead -> str "unknown" - - diff --git a/library/impargs.ml b/library/impargs.ml index c7faff33c..0126c4ad7 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -14,7 +14,6 @@ open Term open Reduction open Declarations open Environ -open Inductive open Libobject open Lib open Pp diff --git a/library/lib.ml b/library/lib.ml index 31f983595..10b4915a2 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -446,10 +446,6 @@ let section_segment_of_constant con = let section_segment_of_mutual_inductive kn = Names.Mindmap.find kn (snd (pi3 (List.hd !sectab))) -let rec list_mem_assoc x = function - | [] -> raise Not_found - | (a, _) :: l -> Names.Id.equal a x || list_mem_assoc x l - let section_instance = function | VarRef id -> if List.exists (fun (id',_,_,_) -> Names.id_eq id id') diff --git a/library/universes.ml b/library/universes.ml index 9c8d8a512..be49294a2 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -10,9 +10,7 @@ open Util open Pp open Names open Term -open Context open Environ -open Locus open Univ type universe_constraint_type = ULe | UEq | ULub @@ -471,12 +469,8 @@ let add_list_map u t map = match rm with Some t -> rm | None -> None) l r in LMap.add u d' lr -let find_list_map u map = - try LMap.find u map with Not_found -> [] - module UF = LevelUnionFind -type universe_full_subst = (universe_level * universe) list - + (** Precondition: flexible <= ctx *) let choose_canonical ctx flexible algs s = let global = LSet.diff s ctx in @@ -499,8 +493,6 @@ let choose_canonical ctx flexible algs s = let canon = LSet.choose algs in canon, (global, rigid, LSet.remove canon flexible) -open Universe - let subst_puniverses subst (c, u as cu) = let u' = Instance.subst subst u in if u' == u then cu else (c, u') @@ -531,9 +523,6 @@ let subst_univs_fn_puniverses lsubst (c, u as cu) = let u' = Instance.subst_fn lsubst u in if u' == u then cu else (c, u') -let subst_univs_puniverses subst cu = - subst_univs_fn_puniverses (Univ.level_subst_of (Univ.make_subst subst)) cu - let nf_evars_and_universes_gen f subst = let lsubst = Univ.level_subst_of subst in let rec aux c = @@ -557,16 +546,10 @@ let nf_evars_and_universes_gen f subst = | _ -> map_constr aux c in aux -let nf_evars_and_universes_subst f subst = - nf_evars_and_universes_gen f (Univ.make_subst subst) - let nf_evars_and_universes_opt_subst f subst = let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in nf_evars_and_universes_gen f subst -let subst_univs_full_constr subst c = - nf_evars_and_universes_subst (fun _ -> None) subst c - let fresh_universe_context_set_instance ctx = if ContextSet.is_empty ctx then LMap.empty, ctx else @@ -652,16 +635,6 @@ let pr_universe_body = function let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body -let is_defined_var u l = - try - match LMap.find u l with - | Some _ -> true - | None -> false - with Not_found -> false - -let subst_univs_subst u l s = - LMap.add u l s - exception Found of Level.t let find_inst insts v = try LMap.iter (fun k (enf,alg,v') -> @@ -669,13 +642,6 @@ let find_inst insts v = insts; raise Not_found with Found l -> l -let add_inst u (enf,b,lbound) insts = - match lbound with - | Some v -> LMap.add u (enf,b,v) insts - | None -> insts - -exception Stays - let compute_lbound left = (** The universe variable was not fixed yet. Compute its level using its lower bound. *) @@ -693,11 +659,6 @@ let compute_lbound left = else None)) None left -let maybe_enforce_leq lbound u cstrs = - match lbound with - | Some lbound -> enforce_leq lbound (Universe.make u) cstrs - | None -> cstrs - let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) = if enforce then let inst = Universe.make u in @@ -941,9 +902,6 @@ let simplify_universe_context (univs,csts) = let is_small_leq (l,d,r) = Level.is_small l && d == Univ.Le -let is_prop_leq (l,d,r) = - Level.equal Level.prop l && d == Univ.Le - (* Prop < i <-> Set+1 <= i <-> Set < i *) let translate_cstr (l,d,r as cstr) = if Level.equal Level.prop l && d == Univ.Lt then diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 4e1806f5a..6177f22f3 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -10,7 +10,6 @@ (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) open Errors -open Names open Term open Ccalgo diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2de0fe717..73c050bb2 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -468,8 +468,6 @@ let congruence_tac depth l = might be slow now, let's rather do something equivalent to a "simple apply refl_equal" *) -let simple_reflexivity () = apply (Universes.constr_of_global _refl_equal) - (* The [f_equal] tactic. It mimics the use of lemmas [f_equal], [f_equal2], etc. diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 11b120c41..076107450 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -21,7 +21,6 @@ open Reductionops open Formula open Sequent open Names -open Globnames open Misctypes let compare_instance inst1 inst2= diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f4a062732..8c3033d0c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -17,19 +17,6 @@ open Misctypes exception Toberemoved_with_rel of int*constr exception Toberemoved -let pr_elim_scheme el = - let env = Global.env () in - let msg = str "params := " ++ Printer.pr_rel_context env el.params in - let env = Environ.push_rel_context el.params env in - let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in - let env = Environ.push_rel_context el.predicates env in - let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in - let env = Environ.push_rel_context el.branches env in - let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in - let env = Environ.push_rel_context el.args env in - msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl - - let observe s = if do_observe () then Pp.msg_debug s @@ -270,10 +257,6 @@ let change_property_sort toSort princ princName = ) princ_info.params - -let pp_dur time time' = - str (string_of_float (System.time_difference time time')) - let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (compute_elim_sig old_princ_type).nparams in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d8f006f51..961266c9c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -10,7 +10,6 @@ open Term open Vars open Namegen open Environ -open Declareops open Entries open Pp open Names @@ -125,7 +124,6 @@ let lt = function () -> (coq_base_constant "lt") let le = function () -> (coq_base_constant "le") let ex = function () -> (coq_base_constant "ex") let nat = function () -> (coq_base_constant "nat") -let coq_sig = function () -> (coq_base_constant "sig") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded" diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 1c9796b4d..d93574b47 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -687,7 +687,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1), (fst (decompose_app_vect (substl ks h'))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) = +(*and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (exp,projs) when Array.length projs > 0 -> @@ -703,7 +703,7 @@ and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) = (Stack.append_app_list sk2 Stack.empty) else raise (Failure "") with Failure _ -> UnifFailure(evd,NotSameHead)) - | _ -> UnifFailure (evd,NotSameHead) + | _ -> UnifFailure (evd,NotSameHead)*) (* Profiling *) let evar_conv_x = diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 7222085e1..66d65bab6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -7,7 +7,6 @@ (************************************************************************) open Util -open Pp open Errors open Names open Term @@ -1194,9 +1193,6 @@ exception NotEnoughInformationEvarEvar of constr exception OccurCheckIn of evar_map * constr exception MetaOccurInBodyInternal -let fast_stats = ref 0 -let not_fast_stats = ref 0 - let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let aliases = make_alias_map env in let evdref = ref evd in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0a9b37698..a842134df 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -126,10 +126,6 @@ let nf_evar_map_undefined evm = (* Auxiliary functions for the conversion algorithms modulo evars *) -let has_flexible_level evd l = - let a = Univ.Instance.to_array l in - Array.exists (fun l -> Evd.is_flexible_level evd l) a - let has_undefined_evars or_sorts evd t = let rec has_ev t = match kind_of_term t with @@ -823,35 +819,6 @@ let pr_tycon env = function open Declarations -let get_template_constructor_type evdref (ind, i) n = - let mib,oib = Global.lookup_inductive ind in - let ar = - match oib.mind_arity with - | RegularArity _ -> assert false - | TemplateArity templ -> templ - in - let ty = oib.mind_user_lc.(pred i) in - let subst = Inductive.ind_subst (fst ind) mib Univ.Instance.empty in - let ty = substl subst ty in - let rec aux l ty n = - match l, kind_of_term ty with - | None :: l, Prod (na, t, t') -> - mkProd (na, t, aux l t' (pred n)) - | Some u :: l, Prod (na, t, t') -> - let u' = evd_comb0 (new_univ_variable Evd.univ_flexible) evdref in - (* evdref := set_leq_sort !evdref u'l (Type u); *) - let s = Univ.LMap.add u - (Option.get (Univ.Universe.level u')) Univ.LMap.empty in - let dom = subst_univs_level_constr s t in - (* let codom = subst_univs_level_constr s t' in *) - mkProd (na, dom, aux l t' (pred n)) - | l, LetIn (na, t, b, t') -> - mkLetIn (na, t, b, aux l t' n) - | _ :: _, _ -> assert false (* All params should be abstracted by a forall or a let-in *) - | [], _ -> ty - in aux ar.template_param_levels ty n - - let get_template_constructor_type evdref (ind, i) n = let mib,oib = Global.lookup_inductive ind in let ar = diff --git a/pretyping/evd.ml b/pretyping/evd.ml index e36e16c05..53d1a8a0e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -954,8 +954,6 @@ let evar_universe_context d = d.universes let universe_context_set d = d.universes.uctx_local -let universes evd = evd.universes.uctx_universes - let universe_context evd = Univ.ContextSet.to_context evd.universes.uctx_local @@ -1088,35 +1086,11 @@ let is_eq_sort s1 s2 = if Univ.Universe.equal u1 u2 then None else Some (u1, u2) -let is_univ_var_or_set u = - not (Option.is_empty (Univ.universe_level u)) - -type universe_global = - | LocalUniv of Univ.universe_level - | GlobalUniv of Univ.universe_level - -type universe_kind = - | Algebraic of Univ.universe - | Variable of universe_global * bool - -let is_univ_level_var (us, cst) algs u = - match Univ.universe_level u with - | Some l -> - let glob = if Univ.LSet.mem l us then LocalUniv l else GlobalUniv l in - Variable (glob, Univ.LSet.mem l algs) - | None -> Algebraic u - let normalize_universe evd = let vars = ref evd.universes.uctx_univ_variables in let normalize = Universes.normalize_universe_opt_subst vars in normalize -let memo_normalize_universe evd = - let vars = ref evd.universes.uctx_univ_variables in - let normalize = Universes.normalize_universe_opt_subst vars in - (fun () -> {evd with universes = {evd.universes with uctx_univ_variables = !vars}}), - normalize - let normalize_universe_instance evd l = let vars = ref evd.universes.uctx_univ_variables in let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in @@ -1178,9 +1152,6 @@ let check_leq evd s s' = let subst_univs_context_with_def def usubst (ctx, cst) = (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) -let subst_univs_context usubst ctx = - subst_univs_context_with_def (Univ.LMap.universes usubst) (Univ.make_subst usubst) ctx - let normalize_evar_universe_context_variables uctx = let normalized_variables, undef, def, subst = Universes.normalize_univ_variables uctx.uctx_univ_variables @@ -1195,14 +1166,6 @@ let normalize_evar_universe_context_variables uctx = (* let normalize_evar_universe_context_variables = *) (* Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *) -let mark_undefs_as_rigid uctx = - let vars' = - Univ.LMap.fold (fun u v acc -> - if v == None && not (Univ.LSet.mem u uctx.uctx_univ_algebraic) - then acc else Univ.LMap.add u v acc) - uctx.uctx_univ_variables Univ.LMap.empty - in { uctx with uctx_univ_variables = vars' } - let mark_undefs_as_nonalg uctx = let vars' = Univ.LMap.fold (fun u v acc -> @@ -1239,16 +1202,6 @@ let refresh_undefined_universes evd = let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in evd', subst -let constraints_universes c = - Univ.Constraint.fold (fun (l',d,r') acc -> Univ.LSet.add l' (Univ.LSet.add r' acc)) - c Univ.LSet.empty - -let is_undefined_universe_variable l vars = - try (match Univ.LMap.find l vars with - | Some u -> false - | None -> true) - with Not_found -> false - let normalize_evar_universe_context uctx = let rec fixpoint uctx = let ((vars',algs'), us') = @@ -1275,10 +1228,6 @@ let nf_univ_variables evd = let evd' = {evd with universes = uctx'} in evd', subst -let normalize_univ_level fullsubst u = - try Univ.LMap.find u fullsubst - with Not_found -> Univ.Universe.make u - let nf_constraints evd = let subst, uctx' = normalize_evar_universe_context_variables evd.universes in let uctx' = normalize_evar_universe_context uctx' in @@ -1299,7 +1248,6 @@ let add_universe_name evd s l = {evd with universes = {evd.universes with uctx_names = names'}} let universes evd = evd.universes.uctx_universes -let constraints evd = evd.universes.uctx_universes (* Conversion w.r.t. an evar map and its local universes. *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 43552ef54..21395af02 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -14,7 +14,6 @@ open Term open Vars open Context open Termops -open Namegen open Declarations open Declareops open Environ diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 6c490d7b9..8b9e6e633 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -38,7 +38,6 @@ let default_type_ident = Id.of_string default_type_string let default_non_dependent_string = "H" let default_non_dependent_ident = Id.of_string default_non_dependent_string -let default_dependent_string = "x" let default_dependent_ident = Id.of_string "x" (**********************************************************************) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5ae49e563..91b851d12 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -288,16 +288,6 @@ let pretype_global rigid env evd gr us = in Evd.fresh_global ~rigid ?names:instance env evd gr -let is_template_polymorphic_constructor env c = - match kind_of_term c with - | Construct ((ind, i), u) -> Environ.template_polymorphic_ind ind env - | _ -> false - -let is_template_polymorphic_constructor env c = - match kind_of_term c with - | Construct ((ind, i), u) -> Environ.template_polymorphic_ind ind env - | _ -> false - let pretype_ref loc evdref env ref us = match ref with | VarRef id -> diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 7250217d6..35ac90de5 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -145,14 +145,6 @@ type cs_pattern = | Sort_cs of sorts_family | Default_cs -let eq_obj_typ o1 o2 = - Constr.equal o1.o_DEF o2.o_DEF && - Int.equal o1.o_INJ o2.o_INJ && - List.equal Constr.equal o1.o_TABS o2.o_TABS && - List.equal Constr.equal o1.o_TPARAMS o2.o_TPARAMS && - Int.equal o1.o_NPARAMS o2.o_NPARAMS && - List.equal Constr.equal o1.o_TCOMPS o2.o_TCOMPS - let eq_cs_pattern p1 p2 = match p1, p2 with | Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2 | Prod_cs, Prod_cs -> true @@ -241,8 +233,6 @@ let pr_cs_pattern = function | Default_cs -> str "_" | Sort_cs s -> Termops.pr_sort_family s -let pr_pattern (p,c) = pr_cs_pattern p - let open_canonical_structure i (_,o) = if Int.equal i 1 then let lo = compute_canonical_projections o in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index fb426efed..c9d4e388d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -736,10 +736,6 @@ let fix_recarg ((recindices,bodynum),_) stack = with Not_found -> None -type 'a reduced_state = - | NotReducible - | Reduced of constr - (** Generic reduction function with environment Here is where unfolded constant are stored in order to be @@ -1082,13 +1078,6 @@ let whd_betadeltaiota_stack env = let whd_betadeltaiota env = red_of_state_red (whd_betadeltaiota_state env) -let whd_betadeltaiota_state_using ts env = - raw_whd_state_gen (Closure.RedFlags.red_add_transparent betadeltaiota ts) env -let whd_betadeltaiota_stack_using ts env = - stack_red_of_state_red (whd_betadeltaiota_state_using ts env) -let whd_betadeltaiota_using ts env = - red_of_state_red (whd_betadeltaiota_state_using ts env) - let whd_betadeltaiotaeta_state env = raw_whd_state_gen betadeltaiotaeta env let whd_betadeltaiotaeta_stack env = stack_red_of_state_red (whd_betadeltaiotaeta_state env) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 53c2603d8..aa33c3286 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -16,7 +16,6 @@ open Inductiveops open Names open Reductionops open Environ -open Declarations open Termops type retype_error = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b405afa93..a32d54b5e 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -59,11 +59,6 @@ let value_of_evaluable_ref env evref u = raise (Invalid_argument "value_of_evaluable_ref")) | EvalVarRef id -> Option.get (pi2 (lookup_named id env)) -let constr_of_evaluable_ref evref u = - match evref with - | EvalConstRef con -> mkConstU (con,u) - | EvalVarRef id -> mkVar id - let evaluable_of_global_reference env = function | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst | VarRef id when is_evaluable_var env id -> EvalVarRef id diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 363292ec0..d9cd58cea 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -494,13 +494,6 @@ let occur_meta_or_existential c = | _ -> iter_constr occrec c in try occrec c; false with Occur -> true -let occur_const s c = - let rec occur_rec c = match kind_of_term c with - | Const (sp,_) when sp=s -> raise Occur - | _ -> iter_constr occur_rec c - in - try occur_rec c; false with Occur -> true - let occur_evar n c = let rec occur_rec c = match kind_of_term c with | Evar (sp,_) when Evar.equal sp n -> raise Occur diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6fa5b8896..d89731147 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -375,11 +375,6 @@ let pr_priority = function | None -> mt () | Some i -> spc () ++ str "|" ++ spc () ++ int i -let pr_poly p = - if Flags.is_universe_polymorphism () then - if not p then str"Monomorphic " else mt () - else if p then str"Polymorphic " else mt () - (**************************************) (* Pretty printer for vernac commands *) (**************************************) diff --git a/printing/printer.ml b/printing/printer.ml index cb10f9661..3b5c80c62 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -727,8 +727,6 @@ let pr_assumptionset env s = ] in prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums) -open Typeclasses - let xor a b = (a && not b) || (not a && b) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 695e8ab6e..d58d1f5a0 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -7,9 +7,7 @@ (************************************************************************) open Util -open Names open Namegen -open Term open Termops open Environ open Reductionops diff --git a/stm/stm.ml b/stm/stm.ml index 5733b0c32..85c3838dc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -214,7 +214,6 @@ module VCS : sig val goals : id -> int -> unit val set_state : id -> state -> unit val get_state : id -> state option - val forget_state : id -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : start:id -> stop:id -> vcs @@ -366,7 +365,6 @@ end = struct | None -> raise Vcs_aux.Expired let set_state id s = (get_info id).state <- Some s let get_state id = (get_info id).state - let forget_state id = (get_info id).state <- None let reached id b = let info = get_info id in if b then info.n_reached <- info.n_reached + 1 @@ -690,19 +688,9 @@ end = struct Stateid.t * Stateid.t * std_ppcmds * (Stateid.t * State.frozen_state) list | RespFeedback of Interface.feedback - | RespGetCounterFreshLocalUniv | RespGetCounterNewUnivLevel - let pr_response = function - | RespBuiltProof _ -> "Sucess" - | RespError _ -> "Error" - | RespFeedback { Interface.id = Interface.State id } -> - "Feedback on " ^ Stateid.to_string id - | RespFeedback _ -> assert false - | RespGetCounterFreshLocalUniv -> "GetCounterFreshLocalUniv" - | RespGetCounterNewUnivLevel -> "GetCounterNewUnivLevel" type more_data = - | MoreDataLocalUniv of Univ.universe list | MoreDataUnivLevel of Univ.universe_level list type task = @@ -987,7 +975,6 @@ end = struct Pp.feedback (Interface.InProgress ~-1) *) last_task := None; raise KillRespawn - | _, RespGetCounterFreshLocalUniv -> assert false (* Deprecated function *) (* marshal_more_data oc (MoreDataLocalUniv *) (* (CList.init 10 (fun _ -> Universes.fresh_local_univ ()))); *) (* loop () *) @@ -1090,7 +1077,7 @@ end = struct Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response !slave_oc RespGetCounterNewUnivLevel; match unmarshal_more_data !slave_ic with - | MoreDataUnivLevel l -> l | _ -> assert false)); + | MoreDataUnivLevel l -> l)); let working = ref false in slave_handshake (); while true do diff --git a/tactics/auto.ml b/tactics/auto.ml index aa70d55cc..4f5f53ef0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -141,12 +141,6 @@ type search_entry = stored_data list * stored_data list * Bounded_net.t let empty_se = ([],[],Bounded_net.create ()) -let eq_constr_or_reference x y = - match x, y with - | IsConstr (x,_), IsConstr (y,_) -> eq_constr x y - | IsGlobRef x, IsGlobRef y -> eq_gr x y - | _, _ -> false - let eq_pri_auto_tactic (_, x) (_, y) = if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then match x.code,y.code with @@ -189,11 +183,6 @@ let is_transparent_gr (ids, csts) = function let dummy_goal = Goal.V82.dummy_goal -let instantiate_constr_or_ref env sigma c = - let c, ctx = Universes.fresh_global_or_constr_instance env c in - let cty = Retyping.get_type_of env sigma c in - (c, cty), ctx - let strip_params env c = match kind_of_term c with | App (f, args) -> @@ -875,10 +864,6 @@ let (forward_intern_tac, extern_intern_tac) = Hook.make () type hnf = bool -let pr_hint_term = function - | IsConstr (c,_) -> pr_constr c - | IsGlobRef gr -> pr_global gr - type hints_entry = | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index a95d71443..02dded782 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -9,11 +9,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Util -open Names open Locus -open Tacexpr open Misctypes -open Tacinterp DECLARE PLUGIN "coretactics" diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index bb7d2f0d2..fd5310e04 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -211,7 +211,7 @@ module SearchProblem = struct let success s = List.is_empty (sig_it s.tacres) - let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) +(* let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) *) let filter_tactics glls l = (* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 617475bb7..9b600409a 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -17,7 +17,6 @@ open Term open Indrec open Declarations open Typeops -open Termops open Ind_tables (* Induction/recursion schemes *) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 7909b669b..c18fd31d0 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -82,8 +82,6 @@ let solveNoteqBranch side = let make_eq () = (*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) -let make_eq_refl () = -(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ()) let mkDecideEqGoal eqonleft op rectype c1 c2 = let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index dc41cf8e3..a2a8675a8 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -72,9 +72,6 @@ let glob_occs ist l = l let subst_occs evm l = l -type occurrences_or_var = int list or_var -type occurrences = int list - ARGUMENT EXTEND occurrences PRINTED BY pr_int_list_full diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 130e66720..a8bcec288 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -387,12 +387,6 @@ let match_eq eqn eq_pat = let no_check () = true let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module -let build_coq_jmeq_data_in env = - build_coq_jmeq_data (), Univ.ContextSet.empty - -let build_coq_identity_data_in env = - build_coq_identity_data (), Univ.ContextSet.empty - let equalities = [coq_eq_pattern, no_check, build_coq_eq_data; coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data; @@ -442,11 +436,6 @@ let dest_nf_eq gls eqn = (*** Sigma-types *) -(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *) -let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ] -let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref -let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref - let match_sigma ex = match kind_of_term ex with | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_exist_ref) f -> diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 7309e2275..b4b8d468c 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -36,12 +36,7 @@ open Goal open Environ open Tacinterp open Termops -open Genarg -open Extraargs -open Pcoq.Constr -open Entries open Libnames -open Evarutil (** Typeclass-based generalized rewriting. *) @@ -76,7 +71,6 @@ let find_global dir s = (** Global constants. *) -let gen_reference dir s = Coqlib.gen_reference "rewrite" dir s let coq_eq_ref = find_reference ["Init"; "Logic"] "eq" let coq_eq = find_global ["Init"; "Logic"] "eq" let coq_f_equal = find_global ["Init"; "Logic"] "f_equal" @@ -118,13 +112,6 @@ let new_cstr_evar (evd,cstrs) env t = let e_new_cstr_evar evars env t = let evd', t = new_cstr_evar !evars env t in evars := evd'; t -let new_goal_evar (evd,cstrs) env t = - let evd', t = Evarutil.new_evar evd env t in - (evd', cstrs), t - -let e_new_goal_evar evars env t = - let evd', t = new_goal_evar !evars env t in evars := evd'; t - (** Building or looking up instances. *) let extends_undefined evars evars' = @@ -161,7 +148,6 @@ module GlobalBindings (M : sig val relation : string list * string val app_poly : env -> evars -> (evars -> evars * constr) -> constr array -> evars * constr val arrow : evars -> evars * constr - val coq_inverse : evars -> evars * constr end) = struct open M let relation : evars -> evars * constr = find_global (fst relation) (snd relation) @@ -608,14 +594,6 @@ let solve_remaining_by by env prf = indep env.evd in { env with evd = evd' }, prf -let extend_evd sigma ext sigma' = - Evar.Set.fold (fun i acc -> - Evd.add acc i (Evarutil.nf_evar_info sigma' (Evd.find sigma' i))) - ext sigma - -let shrink_evd sigma ext = - Evar.Set.fold (fun i acc -> Evd.remove acc i) ext sigma - let no_constraints cstrs = fun ev _ -> not (Evar.Set.mem ev cstrs) @@ -707,10 +685,6 @@ let make_eq () = let make_eq_refl () = (*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ()) -let get_rew_rel r = match r.rew_prf with - | RewPrf (rel, prf) -> rel - | RewCast c -> mkApp (make_eq (),[| r.rew_car; r.rew_from; r.rew_to |]) - let get_rew_prf r = match r.rew_prf with | RewPrf (rel, prf) -> rel, prf | RewCast c -> @@ -1289,25 +1263,6 @@ module Strategies = Some (Some { rew_car = ty; rew_from = t; rew_to = t'; rew_prf = RewCast ckind; rew_evars = evars }) - let fold c : strategy = - fun env avoid t ty cstr evars -> -(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *) - let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in - let unfolded = - try Tacred.try_red_product env sigma c - with e when Errors.noncritical e -> - error "fold: the term is not unfoldable !" - in - try - let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) - unfolded t in - let c' = Evarutil.nf_evar sigma c in - Some (Some { rew_car = ty; rew_from = t; rew_to = c'; - rew_prf = RewCast DEFAULTcast; - rew_evars = (sigma, snd evars) }) - with e when Errors.noncritical e -> None - - let fold_glob c : strategy = fun env avoid t ty cstr evars -> (* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *) @@ -1426,9 +1381,6 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul | Some None -> Some None | None -> None -let rewrite_refine (evd,c) = - Tacmach.refine c - let cl_rewrite_clause_tac ?abs strat meta clause gl = let evartac evd = Refiner.tclEVARS (Evd.clear_metas evd) in let treat res = @@ -1582,30 +1534,11 @@ let cl_rewrite_clause_strat strat clause = let cl_rewrite_clause l left2right occs clause gl = cl_rewrite_clause_strat (rewrite_with (general_rewrite_unif_flags ()) l left2right occs) clause gl -let occurrences_of = function - | n::_ as nl when n < 0 -> (false,List.map abs nl) - | nl -> - if List.exists (fun n -> n < 0) nl then - error "Illegal negative occurrence number."; - (true,nl) - -open Extraargs - -let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars -> - let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in - apply_lemma (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings)) - l2r None occs env avoid t ty cstr (evd, cstrevars evars) - let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars -> let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in apply_lemma (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings)) l2r None occs env avoid t ty cstr (evd, cstrevars evars) -let interp_constr_list env sigma = - List.map (fun c -> - let evd, c = Constrintern.interp_open_constr sigma env c in - (evd, (c, NoBindings)), true, None) - let interp_glob_constr_list env sigma = List.map (fun c -> let evd, c = Pretyping.understand_tcc sigma env c in @@ -2112,74 +2045,6 @@ let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity -let implify id gl = - let (_, b, ctype) = pf_get_hyp gl id in - let binders,concl = decompose_prod_assum ctype in - let evm, ctype' = - match binders with - | (_, None, ty as hd) :: tl when noccurn 1 concl -> - let env = Environ.push_rel_context tl (pf_env gl) in - let sigma = project gl in - let tyhd = Retyping.get_type_of env sigma ty - and tyconcl = Retyping.get_type_of (Environ.push_rel hd env) sigma concl in - let ((sigma,_), app), unfold = - PropGlobal.arrow_morphism env (sigma, Evar.Set.empty) tyhd - (subst1 mkProp tyconcl) ty (subst1 mkProp concl) - in - sigma, it_mkProd_or_LetIn app tl - | _ -> project gl, ctype - in tclTHEN (Refiner.tclEVARS evm) (Tacmach.convert_hyp (id, b, ctype')) gl - -let rec fold_matches env sigma c = - map_constr_with_full_binders Environ.push_rel - (fun env c -> - match kind_of_term c with - | Case _ -> - let cst, env, c', _eff = fold_match ~force:true env sigma c in - fold_matches env sigma c' - | _ -> fold_matches env sigma c) - env c - -let fold_match_tac c gl = - let _, _, c', eff = fold_match ~force:true (pf_env gl) (project gl) c in - let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in - change (Some (snd (Patternops.pattern_of_constr (project gl) c))) c' onConcl gl - -let fold_matches_tac c gl = - let c' = fold_matches (pf_env gl) (project gl) c in - (* let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in *) - change (Some (snd (Patternops.pattern_of_constr (project gl) c))) c' onConcl gl - -let myapply id l gl = - let gr = id in - let _, impls = List.hd (Impargs.implicits_of_global gr) in - let env = pf_env gl in - let evars = ref (project gl) in - let evd, ty = fresh_global env !evars gr in - let _ = evars := evd in - let app = - let rec aux ty impls args args' = - match impls, kind_of_term ty with - | Some (_, _, (_, _)) :: impls, Prod (n, t, t') -> - let arg = Evarutil.e_new_evar evars env t in - aux (subst1 arg t') impls args (arg :: args') - | None :: impls, Prod (n, t, t') -> - (match args with - | [] -> - if dependent (mkRel 1) t' then - let arg = Evarutil.e_new_evar evars env t in - aux (subst1 arg t') impls args (arg :: args') - else - let arg = Evarutil.mk_new_meta () in - evars := meta_declare (destMeta arg) t !evars; - aux (subst1 arg t') impls args (arg :: args') - | arg :: args -> - aux (subst1 arg t') impls args (arg :: args')) - | _, _ -> mkApp (Universes.constr_of_global gr, Array.of_list (List.rev args')) - in aux ty impls l [] - in - tclTHEN (Refiner.tclEVARS !evars) (apply app) gl - let get_lemma_proof f env evm x y = let (evm, _), c = f env (evm,Evar.Set.empty) x y in evm, c diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 35952c9dd..f68f75359 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -43,10 +43,6 @@ let error_syntactic_metavariables_not_allowed loc = let error_tactic_expected loc = user_err_loc (loc,"",str "Tactic expected.") -let skip_metaid = function - | AI x -> x - | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc - (** Generic arguments *) type glob_sign = Genintern.glob_sign = { diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b7018fe45..1d76f4afd 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -294,9 +294,6 @@ let interp_ident = interp_ident_gen false let interp_fresh_ident = interp_ident_gen true let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) -let interp_global ist gl gr = - Evd.fresh_global (pf_env gl) (project gl) gr - (* Interprets an optional identifier which must be fresh *) let interp_fresh_name ist env = function | Anonymous -> Anonymous @@ -578,14 +575,6 @@ let interp_auto_lemmas ist env sigma lems = let pf_interp_type ist gl = interp_type ist (pf_env gl) (project gl) -let new_interp_type ist c k = - let open Proofview.Goal in - let open Proofview.Notations in - Proofview.Goal.raw_enter begin fun gl -> - let (sigma, c) = interp_type ist (env gl) (sigma gl) c in - Proofview.V82.tclEVARS sigma <*> k c - end - (* Interprets a reduction expression *) let interp_unfold ist env (occs,qid) = (interp_occurrences ist occs,interp_evaluable ist env qid) @@ -953,8 +942,6 @@ struct Proofview.tclDISPATCHL (List.map f l) >>= fun l -> Proofview.tclUNIT (Depends (List.concat l)) - let goal = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l) - let enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index aa090b715..4dd4b0aa8 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -15,7 +15,6 @@ open Misctypes open Globnames open Term open Genredexpr -open Inductiveops open Patternops open Pretyping diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index cc1528797..48fd44b4a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -224,6 +224,8 @@ module New : sig val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic + val onHyps : ([ `NF ] Proofview.Goal.t -> named_context) -> + (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic val tryAllHyps : (identifier -> unit tactic) -> unit tactic diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 2d9b4da96..bdacf85a8 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -11,7 +11,6 @@ open Term open Hipattern open Names -open Globnames open Pp open Genarg open Stdarg diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e05f4bcfe..f8d7a197b 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -337,11 +337,11 @@ struct | _ -> assert false (* debug *) - let rec pr_term_pattern p = +(* let rec pr_term_pattern p = (fun pr_t -> function | Term t -> pr_t t | Meta m -> str"["++Pp.int (Obj.magic m)++str"]" - ) (pr_dconstr pr_term_pattern) p + ) (pr_dconstr pr_term_pattern) p*) let search_pat cpat dpat dn = let whole_c = cpat in diff --git a/toplevel/command.ml b/toplevel/command.ml index d28445f17..13696a17c 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -228,9 +228,6 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma in (gr,inst,Lib.is_modtype_strict ()) -let declare_assumptions_hook = ref ignore -let set_declare_assumptions_hook = (:=) declare_assumptions_hook - let interp_assumption evdref env bl c = let c = prod_constr_expr c bl in let ty, impls = interp_type_evars_impls evdref env c in @@ -585,9 +582,6 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -type one_inductive_expr = - lident * local_binder list * constr_expr option * constructor_expr list - let do_mutual_inductive indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) @@ -1079,11 +1073,6 @@ let out_def = function | Some def -> def | None -> error "Program Fixpoint needs defined bodies." -let collect_evars_of_term evd c ty = - let evars = Evar.Set.union (evars_of_term c) (evars_of_term ty) in - Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) - evars Evd.empty - let do_program_recursive local p fixkind fixl ntns = let isfix = fixkind != Obligations.IsCoFixpoint in let (env, rec_sign, evd), fix, info = diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 76d2b89c6..a011fc6a6 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -212,7 +212,7 @@ let display_cmd_header loc com = Pp.flush_all () let rec vernac_com verbosely checknav (loc,com) = - let rec interp = function + let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in let st = save_translator_coqdoc () in -- cgit v1.2.3