diff options
| -rw-r--r-- | checker/term.ml | 10 | ||||
| -rw-r--r-- | kernel/univ.ml | 10 | ||||
| -rw-r--r-- | kernel/univ.mli | 5 | ||||
| -rw-r--r-- | kernel/vars.ml | 6 | ||||
| -rw-r--r-- | kernel/vars.mli | 1 | ||||
| -rw-r--r-- | library/universes.ml | 26 | ||||
| -rw-r--r-- | library/universes.mli | 3 |
7 files changed, 3 insertions, 58 deletions
diff --git a/checker/term.ml b/checker/term.ml index 3372f9b6c..e8cdb03e9 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -397,16 +397,6 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) (* Universe substitutions *) -let subst_univs_puniverses subst = - if Univ.is_empty_level_subst subst then fun c -> c - else - let f = Univ.Instance.subst subst in - fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') - -let subst_univs_fn_puniverses fn = - let f = Univ.Instance.subst_fn fn in - fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') - let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c let subst_univs_fn_constr f c = diff --git a/kernel/univ.ml b/kernel/univ.ml index 256ce5e92..08a7e9454 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1708,7 +1708,6 @@ module Instance : sig val eqeq : t -> t -> bool val subst_fn : universe_level_subst_fn -> t -> t - val subst : universe_level_subst -> t -> t val pr : t -> Pp.std_ppcmds val levels : t -> LSet.t @@ -1763,7 +1762,7 @@ struct let hash = HInstancestruct.hash - let share a = (a, hash a) + let share a = (hcons a, hash a) let empty = hcons [||] @@ -1782,12 +1781,7 @@ struct let subst_fn fn t = let t' = CArray.smartmap fn t in - if t' == t then t else hcons t' - - let subst s t = - let t' = - CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t - in if t' == t then t else hcons t' + if t' == t then t else t' let levels x = LSet.of_array x diff --git a/kernel/univ.mli b/kernel/univ.mli index 9b68dbc8c..25d25fa35 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -272,7 +272,7 @@ sig (** To concatenate two instances, used for discharge *) val equal : t -> t -> bool - (** Equality (note: instances are hash-consed, this is O(1)) *) + (** Equality *) val hcons : t -> t (** Hash-consing. *) @@ -289,9 +289,6 @@ sig val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) - val subst : universe_level_subst -> t -> t - (** Substitution by a level-to-level function. *) - val pr : t -> Pp.std_ppcmds (** Pretty-printing, no comments *) diff --git a/kernel/vars.ml b/kernel/vars.ml index 120c07d30..386a3e8ff 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -216,12 +216,6 @@ let subst_vars subst c = substn_vars 1 subst c (** Universe substitutions *) open Constr -let subst_univs_puniverses subst = - if Univ.is_empty_level_subst subst then fun c -> c - else - let f = Univ.Instance.subst subst in - fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') - let subst_univs_fn_puniverses fn = let f = Univ.Instance.subst_fn fn in fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') diff --git a/kernel/vars.mli b/kernel/vars.mli index b4f616b13..0d5ab07db 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -81,6 +81,5 @@ val subst_univs_constr : universe_subst -> constr -> constr (** Level substitutions for polymorphism. *) -val subst_univs_puniverses : universe_level_subst -> 'a puniverses -> 'a puniverses val subst_univs_level_constr : universe_level_subst -> constr -> constr val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context diff --git a/library/universes.ml b/library/universes.ml index 1c704bc22..788af000b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -508,32 +508,6 @@ let choose_canonical ctx flexible algs s = let canon = LSet.choose algs in canon, (global, rigid, LSet.remove canon flexible) -let subst_puniverses subst (c, u as cu) = - let u' = Instance.subst subst u in - if u' == u then cu else (c, u') - -let nf_evars_and_universes_local f subst = - let rec aux c = - match kind_of_term c with - | Evar (evdk, _ as ev) -> - (match f ev with - | None -> c - | Some c -> aux c) - | Const pu -> - let pu' = subst_puniverses subst pu in - if pu' == pu then c else mkConstU pu' - | Ind pu -> - let pu' = subst_puniverses subst pu in - if pu' == pu then c else mkIndU pu' - | Construct pu -> - let pu' = subst_puniverses subst pu in - if pu' == pu then c else mkConstructU pu' - | Sort (Type u) -> - let u' = Univ.subst_univs_level_universe subst u in - if u' == u then c else mkSort (sort_of_univ u') - | _ -> map_constr aux c - in aux - 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') diff --git a/library/universes.mli b/library/universes.mli index 2fc476732..565f9fb0a 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -191,9 +191,6 @@ val unsafe_type_of_global : Globnames.global_reference -> types (** Full universes substitutions into terms *) -val nf_evars_and_universes_local : (existential -> constr option) -> universe_level_subst -> - constr -> constr - val nf_evars_and_universes_opt_subst : (existential -> constr option) -> universe_opt_subst -> constr -> constr |