From 454a10da9412a5bd6f3661b1f60e17f08289d0e5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Oct 2020 17:13:14 +0200
Subject: [proofs] Support per-definition typing-flags in interactive proofs.

Most cases should be accounted in proof code, however be wary of paths
where `Global.env ()` is used.
---
 proofs/proof.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proofs/proof.mli')

diff --git a/proofs/proof.mli b/proofs/proof.mli
index f487595dac..a527820c7a 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -55,11 +55,13 @@ val data : t -> data
 val start
   :  name:Names.Id.t
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
 
 val dependent_start
   :  name:Names.Id.t
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> Proofview.telescope -> t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
-- 
cgit v1.2.3