diff options
| -rw-r--r-- | vernac/declareDef.ml | 34 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 11 |
2 files changed, 16 insertions, 29 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 7426c128cc..35fb18e292 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -33,34 +33,22 @@ let get_locality id ~kind = function | Local -> true | Global -> false -let declare_global_definition ident ce local k pl imps = - let local = get_locality ident ~kind:"definition" local in - let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in - let gr = ConstRef kn in - let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in - let () = definition_message ident in - gr - let declare_definition ident (local, p, k) ce pl imps hook = let fix_exn = Future.fix_exn_of ce.const_entry_body in - let r = match local with + let gr = match local with | Discharge when Lib.sections_are_opened () -> - let c = SectionLocalDef ce in - let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in - let () = definition_message ident in - let gr = VarRef ident in - let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in - let () = if Proof_global.there_are_pending_proofs () then - warn_definition_not_visible ident - in - gr + 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 + VarRef ident | Discharge | Local | Global -> - declare_global_definition ident ce local k pl imps in - Lemmas.call_hook fix_exn hook local r; r + let local = get_locality ident ~kind:"definition" local in + let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in + ConstRef kn in + let () = maybe_declare_manual_implicits false gr imps in + let () = Declare.declare_univ_binders gr pl in + let () = definition_message ident in + Lemmas.call_hook fix_exn hook local gr; gr let declare_fix ?(opaque = false) (_,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 ce pl imps (Lemmas.mk_hook (fun _ _ -> ())) - diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 455dd86668..8aa459729c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -179,14 +179,14 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let const = adjust_guardness_conditions const do_guard in let k = Kindops.logical_kind_of_goal_kind kind in let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in - let l,r = match locality with + let r = match locality with | Discharge when Lib.sections_are_opened () -> let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in let () = if should_suggest then Proof_using.suggest_variable (Global.env ()) id in - (Local, VarRef id) + VarRef id | Local | Global | Discharge -> let local = match locality with | Local | Discharge -> true @@ -197,11 +197,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in - (locality, ConstRef kn) + ConstRef kn in definition_message id; Declare.declare_univ_binders r (UState.universe_binders uctx); - call_hook (fun exn -> exn) hook l r + call_hook (fun exn -> exn) hook locality r with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -221,12 +221,12 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in + let k = IsAssumption Conjectural in match body with | None -> (match locality with | Discharge -> let impl = false in (* copy values from Vernacentries *) - let k = IsAssumption Conjectural in let univs = match univs with | Polymorphic_const_entry univs -> (* What is going on here? *) @@ -237,7 +237,6 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_, let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> - let k = IsAssumption Conjectural in let local = match locality with | Local -> true | Global -> false |