diff options
| author | Hugo Herbelin | 2018-10-06 18:53:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-15 13:54:12 +0200 |
| commit | a52c53c166c1cc138e2e2189697d126babad1409 (patch) | |
| tree | 1f8ae18e6661be80b59ac4c3aca75b467ddb87d4 | |
| parent | 3d9080dcfa21e2afc9a9cf0ba24146b3e4341edb (diff) | |
Make code of `Lemmas.save` closer to the one of `DeclareDef.declare_definition`.
This is a theoretical change of semantics in the presence of commands
generating a "hook", such as "Coercion c := ...", or "SubClass", or
"Canonical Structure". However, none of these commands have a
"Discharge" effect, so the case was not used.
| -rw-r--r-- | vernac/lemmas.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 455dd86668..55c8b1452c 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) |