diff options
| author | Maxime Dénès | 2019-01-25 17:47:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-05 09:36:51 +0100 |
| commit | 49a545b7606f8bd846d2e3740d0bb3ea1ea6eb38 (patch) | |
| tree | e6697a39eb0cfb7b45a08e88dd08ad2fe7eedadb /vernac/comInductive.ml | |
| parent | 5c1d7fc460d0b98a1dfbcf151079dbacb64c9330 (diff) | |
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.
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index afee2a5868..68ad276113 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -162,7 +162,7 @@ let interp_cstrs env sigma impls mldata arity ind = let sigma, (ctyps'', cimpls) = on_snd List.split @@ List.fold_left_map (fun sigma l -> - interp_type_evars_impls env sigma ~impls l) sigma ctyps' in + interp_type_evars_impls ~program_mode:false env sigma ~impls l) sigma ctyps' in sigma, (cnames, ctyps'', cimpls) let sign_level env evd sign = @@ -358,9 +358,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not then user_err (str "Inductives with uniform parameters may not have attached notations."); let sigma, udecl = interp_univ_decl_opt env0 udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = - interp_context_evars env0 sigma uparamsl in + interp_context_evars ~program_mode:false env0 sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = - interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl + interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in |