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/comAssumption.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/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index f9b73a59eb..a0b0dcf4c8 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -217,7 +217,7 @@ let context_insection sigma ~poly ctx = in let entry = Declare.definition_entry ~univs ~types:t b in let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.Definition UnivNames.empty_binders entry [] + ~kind:Decls.(IsDefinition Definition) UnivNames.empty_binders entry [] in () in |