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. --- library/heads.ml | 14 -------------- library/impargs.ml | 1 - library/lib.ml | 4 ---- library/universes.ml | 44 +------------------------------------------- 4 files changed, 1 insertion(+), 62 deletions(-) (limited to 'library') 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 -- cgit v1.2.3