From bef2e53ae2286d0a7c61697f7a7a71bfdc0a3c99 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 5 Apr 2017 14:49:13 +0200
Subject: Subtyping inference for inductoves and records

Also reinferred after sections discharge
---
 pretyping/inductiveops.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'pretyping/inductiveops.mli')

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index bdb6f996b9..7d89b1b2bd 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -199,3 +199,8 @@ val type_of_inductive_knowing_conclusion :
 
 (********************)
 val control_only_guard : env -> types -> unit
+
+(* inference of subtyping condition for inductive types *)
+
+val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
+  Entries.mutual_inductive_entry
-- 
cgit v1.2.3