From f02f64a21863ce03f2da4ff04cd003051f96801f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 29 Oct 2015 18:18:43 +0100
Subject: Removing some goal unsafeness in inductive schemes.

---
 engine/sigma.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'engine/sigma.mli')

diff --git a/engine/sigma.mli b/engine/sigma.mli
index 6ac56bb3e2..cb948dba59 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -66,6 +66,12 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
 
 (** Polymorphic universes *)
 
+val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env ->
+  'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
+val fresh_constant_instance :
+  Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
+val fresh_inductive_instance :
+  Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
 val fresh_constructor_instance : Environ.env -> 'r t -> constructor ->
   (pconstructor, 'r) sigma
 
-- 
cgit v1.2.3