diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comAssumption.ml | 2 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 5 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 6 |
3 files changed, 7 insertions, 6 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 60086a7861..520df1c21e 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -52,7 +52,7 @@ match scope with in let kind = Decls.IsAssumption kind in let decl = Lib.cwd(), SectionLocalAssum {typ; univs; poly; impl} in - let _ = declare_variable ~name ~kind decl in + let () = declare_variable ~name ~kind decl in let () = assumption_message name in let r = VarRef name in let () = maybe_declare_manual_implicits true r imps in diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 4dcb3db63b..2aa96fa8ed 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -48,8 +48,9 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in let gr = match scope with | Discharge -> - let _ : Libobject.object_name = - declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce) in + let () = + declare_variable ~name ~kind:Decls.(IsDefinition kind) (Lib.cwd(), SectionLocalDef ce) + in VarRef name | Global local -> let kn = declare_constant ~name ~local ~kind:Decls.(IsDefinition kind) (DefinitionEntry ce) in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d0e2e0f935..d6ee0b96f2 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -266,7 +266,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i | Monomorphic_entry univs -> univs in let c = Declare.SectionLocalAssum {typ=t_i; univs; poly; impl} in - let _ = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in + let () = Declare.declare_variable ~name ~kind (Lib.cwd(),c) in (VarRef name,impargs) | Global local -> let kind = Decls.(IsAssumption Conjectural) in @@ -289,7 +289,7 @@ let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i | Discharge -> let const = Declare.definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = Declare.SectionLocalDef const in - let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in + let () = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in (VarRef name,impargs) | Global local -> let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in @@ -499,7 +499,7 @@ let finish_proved env sigma idopt po info = let r = match scope with | Discharge -> let c = Declare.SectionLocalDef const in - let _ = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in + let () = Declare.declare_variable ~name ~kind (Lib.cwd(), c) in let () = if should_suggest then Proof_using.suggest_variable (Global.env ()) name in |