diff options
| author | coqbot-app[bot] | 2020-10-19 10:43:01 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-19 10:43:01 +0000 |
| commit | 5be9faac2dcf44b383e57f95b4fbd558b8bd24b8 (patch) | |
| tree | 8d089ada60a308f58bb63ac628ffbd71257da455 /vernac/comDefinition.mli | |
| parent | 4cb8a7c47972fc15e8f755a99e4a14170580aac1 (diff) | |
| parent | 2b8a11101a1f152f78f0f8c924701e5f3915b4f7 (diff) | |
Merge PR #13166: Fixes #13165: implicit arguments in defined fields of record types not taken into account
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac/comDefinition.mli')
| -rw-r--r-- | vernac/comDefinition.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index d95e64a85f..7420235449 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -14,6 +14,17 @@ open Constrexpr (** {6 Definitions/Let} *) +val interp_definition + : program_mode:bool + -> Environ.env + -> Evd.evar_map + -> Constrintern.internalization_env + -> Constrexpr.local_binder_expr list + -> red_expr option + -> constr_expr + -> constr_expr option + -> Evd.evar_map * (EConstr.t * EConstr.t option) * Impargs.manual_implicits + val do_definition : ?hook:Declare.Hook.t -> name:Id.t |