From fd7448ad0f44ef306d910816d7b6d2f6a303f4a7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 14 May 2013 18:38:14 +0000 Subject: 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 --- kernel/inductive.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/inductive.mli') 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} *) -- cgit v1.2.3