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.
---
 engine/evarutil.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 0e67475778..23b240f1a0 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -38,6 +38,7 @@ type naming_mode =
   | KeepUserNameAndRenameExistingEvenSectionNames
   | KeepExistingNames
   | FailIfConflict
+  | ProgramNaming
 
 val new_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-- 
cgit v1.2.3