diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-14 18:38:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-14 18:38:14 +0000 |
| commit | fd7448ad0f44ef306d910816d7b6d2f6a303f4a7 (patch) | |
| tree | 5a5c51c01bbbaa75a4ddffcca384cdf5cc7d0d2e /kernel/inductive.mli | |
| parent | 23a51bab686dd0ceaa9a87b09beb49d0ee0575c4 (diff) | |
Delayed the computation of parameters in sort polymorphism of
inductive types. This saves some computation, but also allows
incidentally to retype terms with evars without failing if an
inductive type as an argument whose type is an evar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16526 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 9a458f02a..d9841085e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -93,12 +93,12 @@ val check_cofix : env -> cofixpoint -> unit exception SingletonInductiveBecomesProp of Id.t val type_of_inductive_knowing_parameters : ?polyprop:bool -> - env -> one_inductive_body -> types array -> types + env -> one_inductive_body -> types Lazy.t array -> types val max_inductive_sort : sorts array -> universe val instantiate_universes : env -> rel_context -> - polymorphic_arity -> types array -> rel_context * sorts + polymorphic_arity -> types Lazy.t array -> rel_context * sorts (** {6 Debug} *) |