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.

1 files changed, 5 insertions, 4 deletions

diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index e8a2fbdd16..63f72e60bd 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -13,6 +13,7 @@ open Environ
 open Evd
 open EConstr
 open Ltac_pretype
+open Evarutil
 
 (** To embed constr in glob_constr *)
 
@@ -37,7 +38,7 @@ type t
 
 (** Build a pretyping environment from an ltac environment *)
 
-val make : env -> evar_map -> ltac_var_map -> t
+val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
 
 (** Export the underlying environement *)
 
@@ -47,9 +48,9 @@ val vars_of_env : t -> Id.Set.t
 
 (** Push to the environment, returning the declaration(s) with interpreted names *)
 
-val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t
-val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
-val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t array * t
+val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t
+val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
+val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t array * constr array -> t -> Name.t array * t
 
 (** Declare an evar using renaming information *)