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.ml  | 6 ++++--
 engine/evarutil.mli | 1 +
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index db56d0628f..d70c009c6d 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -337,6 +337,7 @@ type naming_mode =
   | KeepUserNameAndRenameExistingEvenSectionNames
   | KeepExistingNames
   | FailIfConflict
+  | ProgramNaming
 
 let push_rel_decl_to_named_context
   ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
@@ -364,7 +365,7 @@ let push_rel_decl_to_named_context
         using this function. For now, we only attempt to preserve the
         old behaviour of Program, but ultimately, one should do something
         about this whole name generation problem. *)
-    if Flags.is_program_mode () then next_name_away na avoid
+    if hypnaming = ProgramNaming then next_name_away na avoid
     else
       (* id_of_name_using_hdchar only depends on the rel context which is empty
          here *)
@@ -372,7 +373,8 @@ let push_rel_decl_to_named_context
   in
   match extract_if_neq id na with
   | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames ||
-                  hypnaming = KeepUserNameAndRenameExistingButSectionNames &&
+                  (hypnaming = KeepUserNameAndRenameExistingButSectionNames ||
+                   hypnaming = ProgramNaming) &&
                   not (is_section_variable id0) ->
       (* spiwack: if [id<>id0], rather than introducing a new
           binding named [id], we will keep [id0] (the name given
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