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.
---
 stm/vernac_classifier.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 42540af991..feb8e2a67f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -56,6 +56,7 @@ let options_affecting_stm_scheduling =
   [ Attributes.universe_polymorphism_option_name;
     stm_allow_nested_proofs_option_name;
     Vernacentries.proof_mode_opt_name;
+    Attributes.program_mode_option_name;
   ]
 
 let classify_vernac e =
-- 
cgit v1.2.3