diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:31:34 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:31:34 +0200 |
commit | 6390887ce1fd32c2180f373f1e701d9488c341f9 (patch) | |
tree | ef53b4077d1b947f7f3064765fa8a609efbb5cab /checker/term.ml | |
parent | 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 (diff) |
Remove unused substitution functions in checker.
Diffstat (limited to 'checker/term.ml')
-rw-r--r-- | checker/term.ml | 74 |
1 files changed, 0 insertions, 74 deletions
diff --git a/checker/term.ml b/checker/term.ml index 3438f497a..1b8177325 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -404,77 +404,6 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) 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 = - let changed = ref false in - let fu = Univ.subst_univs_universe f in - let fi = Univ.Instance.subst_fn (Univ.level_subst_of f) in - let rec aux t = - match t with - | Sort (Type u) -> - let u' = fu u in - if u' == u then t else - (changed := true; Sort (Type u')) - | Const (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; Const (c, u')) - | Ind (i, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; Ind (i, u')) - | Construct (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; Construct (c, u')) - | _ -> map_constr aux t - in - let c' = aux c in - if !changed then c' else c - -let subst_univs_constr subst c = - if Univ.is_empty_subst subst then c - else - let f = Univ.make_subst subst in - subst_univs_fn_constr f c - - -let subst_univs_level_constr subst c = - if Univ.is_empty_level_subst subst then c - else - let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in - let changed = ref false in - let rec aux t = - match t with - | Const (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Const (c, u')) - | Ind (i, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Ind (i, u')) - | Construct (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Construct (c, u')) - | Sort (Type u) -> - let u' = Univ.subst_univs_level_universe subst u in - if u' == u then t else - (changed := true; Sort (Type u')) - | _ -> map_constr aux t - in - let c' = aux c in - if !changed then c' else c - -let subst_univs_level_context s = - map_rel_context (subst_univs_level_constr s) - let subst_instance_constr subst c = if Univ.Instance.is_empty subst then c else @@ -509,9 +438,6 @@ let subst_instance_constr subst c = let c' = aux c in if !changed then c' else c -(* let substkey = Profile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) - let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else map_rel_context (fun x -> subst_instance_constr s x) ctx |