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.

2 files changed, 31 insertions, 28 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c8c38ffe05..24894fc9f5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2328,36 +2328,38 @@ let interp_open_constr env sigma c =
 
 (* Not all evars expected to be resolved and computation of implicit args *)
 
-let interp_constr_evars_gen_impls env sigma
+let interp_constr_evars_gen_impls ?(program_mode=false) env sigma
     ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env sigma c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
-  let sigma, c = understand_tcc env sigma ~expected_type c in
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+  let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
   sigma, (c, imps)
 
-let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls ?program_mode env sigma ~impls WithoutTypeConstraint c
 
-let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c
+let interp_casted_constr_evars_impls ?program_mode env evdref ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen_impls ?program_mode env evdref ~impls (OfType typ) c
 
-let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls env sigma ~impls IsType c
+let interp_type_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls ?program_mode env sigma ~impls IsType c
 
 (* Not all evars expected to be resolved, with side-effect on evars *)
 
-let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c =
+let interp_constr_evars_gen ?(program_mode=false) env sigma ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env sigma c in
-  understand_tcc env sigma ~expected_type c
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+  understand_tcc ~flags env sigma ~expected_type c
 
-let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
+let interp_constr_evars ?program_mode env evdref ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen ?program_mode env evdref WithoutTypeConstraint ~impls c
 
-let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen env sigma ~impls (OfType typ) c
+let interp_casted_constr_evars ?program_mode env sigma ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen ?program_mode env sigma ~impls (OfType typ) c
 
-let interp_type_evars env sigma ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen env sigma IsType ~impls c
+let interp_type_evars ?program_mode env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen ?program_mode env sigma IsType ~impls c
 
 (* Miscellaneous *)
 
@@ -2419,8 +2421,9 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
-let interp_glob_context_evars env sigma k bl =
+let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
   let open EConstr in
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
   let env, sigma, par, _, impls =
     List.fold_left
       (fun (env,sigma,params,n,impls) (na, k, b, t) ->
@@ -2428,7 +2431,7 @@ let interp_glob_context_evars env sigma k bl =
 	 if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
 	 else t
        in
-       let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in
+       let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in
 	match b with
 	    None ->
 	      let d = LocalAssum (na,t) in
@@ -2440,13 +2443,13 @@ let interp_glob_context_evars env sigma k bl =
 	      in
                 (push_rel d env, sigma, d::params, succ n, impls)
 	  | Some b ->
-              let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in
+              let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in
 	      let d = LocalDef (na, c, t) in
                 (push_rel d env, sigma, d::params, n, impls))
       (env,sigma,[],k+1,[]) (List.rev bl)
   in sigma, ((env, par), impls)
 
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
+let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let sigma, x = interp_glob_context_evars env sigma shift bl in
+  let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in
   sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 61acd09d65..2d14a0d0a7 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -113,26 +113,26 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
 
 (** Accepting unresolved evars *)
 
-val interp_constr_evars : env -> evar_map ->
+val interp_constr_evars : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> evar_map * constr
 
-val interp_casted_constr_evars : env -> evar_map ->
+val interp_casted_constr_evars : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> types -> evar_map * constr
 
-val interp_type_evars : env -> evar_map ->
+val interp_type_evars : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> evar_map * types
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-val interp_constr_evars_impls : env -> evar_map ->
+val interp_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
   evar_map * (constr * Impargs.manual_implicits)
 
-val interp_casted_constr_evars_impls : env -> evar_map ->
+val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> types ->
   evar_map * (constr * Impargs.manual_implicits)
 
-val interp_type_evars_impls : env -> evar_map ->
+val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
   evar_map * (types * Impargs.manual_implicits)
 
@@ -158,7 +158,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map *
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
-  ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
+  ?program_mode:bool -> ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map -> local_binder_expr list ->
   evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))