diff options
| author | Gaëtan Gilbert | 2020-02-09 19:49:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-14 16:10:09 +0100 |
| commit | faef5dcc656148273063f25716923d9bd1fe2497 (patch) | |
| tree | 2194a1c038c924da4bea8d449082fe130662af0e /kernel/inductive.mli | |
| parent | 90ccf8e413aea57ec670ea26174d3deffb4036aa (diff) | |
Use thunks to univ instead of lazy constr for template typing
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 8c40c318c5..b690fe1157 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -41,16 +41,22 @@ val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_contex val instantiate_inductive_constraints : mutual_inductive_body -> Instance.t -> Constraint.t -val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained +type param_univs = (unit -> Universe.t) list + +val make_param_univs : Environ.env -> constr array -> param_univs +(** The constr array is the types of the arguments to a template + polymorphic inductive. *) + +val constrained_type_of_inductive : mind_specif puniverses -> types constrained val constrained_type_of_inductive_knowing_parameters : - env -> mind_specif puniverses -> types Lazy.t array -> types constrained + mind_specif puniverses -> param_univs -> types constrained val relevance_of_inductive : env -> inductive -> Sorts.relevance -val type_of_inductive : env -> mind_specif puniverses -> types +val type_of_inductive : mind_specif puniverses -> types val type_of_inductive_knowing_parameters : - env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types + ?polyprop:bool -> mind_specif puniverses -> param_univs -> types val elim_sort : mind_specif -> Sorts.family @@ -117,8 +123,8 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : env -> Constr.rel_context -> - template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t +val instantiate_universes : Constr.rel_context -> + template_arity -> param_univs -> Constr.rel_context * Sorts.t (** {6 Debug} *) |