diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:27:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:27:37 +0200 |
| commit | 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 (patch) | |
| tree | d67a1ead218ca15becb33b605426cb5429323b60 /checker/cic.mli | |
| parent | 0d7cd6eebd5b681f7dcb243e3cda4466e735e025 (diff) | |
Fix checker treatment of inductives using subst_instances instead of subst_univs_levels.
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index c1d7b0d73..2f33c60f5 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -170,7 +170,7 @@ type engagement = ImpredicativeSet type template_arity = { - template_param_levels : Univ.universe option list; + template_param_levels : Univ.universe_level option list; template_level : Univ.universe; } @@ -212,8 +212,6 @@ type constant_body = { const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_constraints : Univ.constraints; - const_native_name : native_name ref; const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; |