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.
---
 pretyping/globEnv.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'pretyping/globEnv.ml')

diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 49a08afe80..d6b204561e 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -38,10 +38,10 @@ type t = {
   lvar : ltac_var_map;
 }
 
-let make env sigma lvar =
+let make ~hypnaming env sigma lvar =
   let get_extra env sigma =
     let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
-    Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
+    Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
       (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
   {
     static_env = env;
@@ -66,32 +66,32 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id =
 
 let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
 
-let push_rel sigma d env =
+let push_rel ~hypnaming sigma d env =
   let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
   let env = {
     static_env = push_rel d env.static_env;
     renamed_env = push_rel d' env.renamed_env;
-    extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra));
+    extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
   d', env
 
-let push_rel_context ?(force_names=false) sigma ctx env =
+let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
   let open Context.Rel.Declaration in
   let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in
   let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in
   let env = {
     static_env = push_rel_context ctx env.static_env;
     renamed_env = push_rel_context ctx' env.renamed_env;
-    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra));
+    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
   ctx', env
 
-let push_rec_types sigma (lna,typarray) env =
+let push_rec_types ~hypnaming sigma (lna,typarray) env =
   let open Context.Rel.Declaration in
   let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
-  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in
+  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e ~hypnaming in (e,d)) env ctxt in
   Array.map get_name ctx, env
 
 let new_evar env sigma ?src ?naming typ =
-- 
cgit v1.2.3