diff options
| author | Maxime Dénès | 2017-07-20 14:39:37 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-20 14:39:37 +0200 |
| commit | f25613e8a2a6c9264650cb0be891bb073979c67d (patch) | |
| tree | 1466b12f4da09840c563fd4ce5b81556c0e09af7 /checker/term.ml | |
| parent | bb13eed99c310970ebb52c56ce785c1879caed66 (diff) | |
| parent | e2e41c94f1f965e8c7d8bd4a93b58774821c2273 (diff) | |
Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: Checker
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/checker/term.ml b/checker/term.ml index 9bcb15bc72..5995dfcc61 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -447,37 +447,3 @@ let subst_instance_constr subst 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 - -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 (sort_of_univ u')) - | _ -> map_constr aux t - in - let c' = aux c in - if !changed then c' else c |