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, 4 insertions, 4 deletions

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 7301e1fff7..73d0be04df 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -84,8 +84,8 @@ match local with
   in
     (gr,inst,Lib.is_modtype_strict ())
 
-let interp_assumption sigma env impls c =
-  let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in
+let interp_assumption ~program_mode sigma env impls c =
+  let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in
   sigma, (ty, impls)
 
 (* When monomorphic the universe constraints are declared with the first declaration only. *)
@@ -131,7 +131,7 @@ let process_assumptions_udecls kind l =
   in
   udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l
 
-let do_assumptions kind nl l =
+let do_assumptions ~program_mode kind nl l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let udecl, l = process_assumptions_udecls kind l in
@@ -147,7 +147,7 @@ let do_assumptions kind nl l =
   in
   (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
-    let sigma,(t,imps) = interp_assumption sigma env ienv c in
+    let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
     let env =
       EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
     let ienv = List.fold_right (fun {CAst.v=id} ienv ->