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 /plugins/funind | |
| 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 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d9b0330e2b..42dc66dcf4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -166,7 +166,7 @@ let build_newrecursive let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1b5286dce4..0c97f9f373 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1518,10 +1518,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open CVars in let env = Global.env() in let evd = Evd.from_env env in - let evd, function_type = interp_type_evars env evd type_of_f in + let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in |