From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 28 Oct 2013 14:08:46 +0100
Subject: Initial work on reintroducing old-style polymorphism for
 compatibility (the stdlib does not compile entirely).

---
 pretyping/inductiveops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.mli')

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 39451ec050..34ddce72b6 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -142,7 +142,7 @@ i*)
 (********************)
 
 val type_of_inductive_knowing_conclusion :
-  env -> Inductive.mind_specif puniverses -> types -> types
+  env -> evar_map -> Inductive.mind_specif puniverses -> types -> evar_map * types
 
 (********************)
 val control_only_guard : env -> types -> unit
-- 
cgit v1.2.3