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.
---
 plugins/funind/indfun.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 158eb96466..071599d9c5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -407,6 +407,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
     | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
       ComDefinition.do_definition
+        ~program_mode:false
 	fname
 	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
-- 
cgit v1.2.3