diff options
| author | Maxime Dénès | 2019-03-28 13:36:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-28 13:36:52 +0100 |
| commit | 688e20c432d2639050a62703e1c566ddfbe42b2a (patch) | |
| tree | 3b34d3bd3b73a42a8eb730a3bb6c0e6a5cb00a5f /vernac/declareDef.ml | |
| parent | 6d0ffe795f6f29730d59c379285201fd46023935 (diff) | |
| parent | 91dfe5163fd4405977ad8fc8fe178ba5bcd73c88 (diff) | |
Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 7dcd098183..052832244b 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -33,12 +33,12 @@ let get_locality id ~kind = function | Local -> true | Global -> false -let declare_definition ident (local, p, k) ?hook_data ce pl imps = +let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with | Discharge when Lib.sections_are_opened () -> let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in - let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in + let () = if Option.has_some ontop then warn_definition_not_visible ident in VarRef ident | Discharge | Local | Global -> let local = get_locality ident ~kind:"definition" local in @@ -57,9 +57,9 @@ let declare_definition ident (local, p, k) ?hook_data ce pl imps = end; gr -let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = +let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition f kind ?hook_data ce pl imps + declare_definition ~ontop f kind ?hook_data ce pl imps let check_definition_evars ~allow_evars sigma = let env = Global.env () in |