From e2e41c94f1f965e8c7d8bd4a93b58774821c2273 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 18 Jul 2017 22:55:28 +0200 Subject: Fixing the checker w.r.t. wrongly used abstract universe contexts. It seems we were not testing the checker on cumulative inductive types, because judging from the code, it would just have exploded in anomalies. Before this patch, the checker was mixing De Bruijn indices with named variables, resulting in ill-formed universe contexts used throughout the checking of cumulative inductive types. This patch also gets rid of a lot of now dead code, and removes abstraction breaking code from the checker. --- checker/term.ml | 34 ---------------------------------- 1 file changed, 34 deletions(-) (limited to 'checker/term.ml') diff --git a/checker/term.ml b/checker/term.ml index 9bcb15bc7..5995dfcc6 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 -- cgit v1.2.3