diff options
| author | Hugo Herbelin | 2020-10-09 19:28:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-16 01:29:19 +0200 |
| commit | 12ea3318943f2a47f45d939aa206acc263a6341d (patch) | |
| tree | eb4269af04dbca16c53d3bed1a879289a987d094 /vernac/comDefinition.mli | |
| parent | 2db3d504378cb6167aadd0d7bccf7bd2341c63c6 (diff) | |
Generalizing and exporting interp_assumption/interp_definition.
This shall be for Record fields consumption.
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 |