From 49a545b7606f8bd846d2e3740d0bb3ea1ea6eb38 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 17:47:03 +0100
Subject: Make Program a regular attribute

We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.

This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
---
 vernac/classes.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/classes.mli')

diff --git a/vernac/classes.mli b/vernac/classes.mli
index 6f61da66cf..7e0ec42625 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -55,6 +55,7 @@ val new_instance :
 
 val declare_new_instance :
   ?global:bool (** Not global by default. *) ->
+  program_mode:bool ->
   Decl_kinds.polymorphic ->
   local_binder_expr list ->
   ident_decl * Decl_kinds.binding_kind * constr_expr ->
-- 
cgit v1.2.3