From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- kernel/cbytegen.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/cbytegen.mli') diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index c0f48641c..48c2e4533 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -10,7 +10,7 @@ val compile : bool -> (* Fail on error with a nice user message, otherwise simpl (** init, fun, fv *) val compile_constant_body : bool -> - env -> constant_universes option -> constant_def -> body_code option + env -> constant_universes -> constant_def -> body_code option (** Shortcut of the previous function used during module strengthening *) -- cgit v1.2.3