diff options
| author | Gaëtan Gilbert | 2019-10-26 21:21:48 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-26 21:21:48 +0200 |
| commit | f508ddcd2cfff152b8d6291d96e4b87ef9fe2ff9 (patch) | |
| tree | a80f8a1646e81bdb94bc74229ef5b42bc24b31ff /vernac/comDefinition.ml | |
| parent | f7659e6c5d197ddeff8509a4aab40316534b3a12 (diff) | |
| parent | 4035b4a66dbd8e29aa933b1e301fbd07815768e4 (diff) | |
Merge PR #10516: [funind] Remove duplicate save function.
Reviewed-by: SkySkimmer
Ack-by: gares
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9745358ba2..5b3f15a08c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -104,4 +104,5 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + let kind = Decls.IsDefinition kind in ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) |