diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-18 22:55:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-19 01:23:54 +0200 |
| commit | e2e41c94f1f965e8c7d8bd4a93b58774821c2273 (patch) | |
| tree | a56b3021616cc46179bc994e52503b91ff82096f /checker/term.mli | |
| parent | 0315a5d93c2de996f5c91bd2af827d3984ec1ad8 (diff) | |
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.
Diffstat (limited to 'checker/term.mli')
| -rw-r--r-- | checker/term.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/checker/term.mli b/checker/term.mli index ccf5b59e0..679a56ee4 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -57,4 +57,3 @@ val eq_constr : constr -> constr -> bool (** Instance substitution for polymorphism. *) val subst_instance_constr : Univ.universe_instance -> constr -> constr val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context -val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr |