diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-07 16:33:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | 0d9a91113c4112eece0680e433f435fdfb39ea4b (patch) | |
| tree | cf90d290a92c02a2297b3a13b77190db9aa4db70 /checker/inductive.mli | |
| parent | b5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff) | |
Getting rid of simple calls to AUContext.instance.
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
Diffstat (limited to 'checker/inductive.mli')
| -rw-r--r-- | checker/inductive.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/checker/inductive.mli b/checker/inductive.mli index 698b8b77c..b8cbda7cf 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -26,8 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool val inductive_is_cumulative : mutual_inductive_body -> bool -val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance - val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context val type_of_inductive : env -> mind_specif puniverses -> constr |