From 1172b52735a299dfc91aee36b30b576dfeff581c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 13 Dec 2017 21:26:48 +0100
Subject: [flags] Make program_mode a parameter for commands in vernac.

This is useful as it allows to reflect program_mode behavior as an attribute.
---
 API/API.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 8386133521..ce33e90296 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -6052,7 +6052,9 @@ end
 
 module ComDefinition :
 sig
-  val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
+  val do_definition :
+    program_mode:bool ->
+    Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
     Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr ->
     Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit
 end
@@ -6134,6 +6136,7 @@ sig
     ?abstract:bool ->
     ?global:bool ->
     ?refine:bool ->
+    program_mode:bool ->
     Decl_kinds.polymorphic ->
     Constrexpr.local_binder_expr list ->
     Vernacexpr.typeclass_constraint ->
-- 
cgit v1.2.3