diff options
| author | Gaëtan Gilbert | 2019-07-02 13:51:49 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-03 17:05:29 +0200 |
| commit | 48a377680f4f3b96f7c19c22f5641877c561f03d (patch) | |
| tree | 5d4e560f19910fcc68c536f0ba97df16c39d4e05 /vernac | |
| parent | 4f0bdf2e19f0562a6cdf3b5ac075326b6e28c1d7 (diff) | |
Declare section variables in direct style "without" an object
The object was mostly for wrangling universes, but we already have the
universe object for that.
It's also used by some code which iterates over objects to find
variables.
Search used to do this but was changed in a previous commit.
Prettyp.print_context and derivatives do this and I don't understand
it enough to fix it, so I kept a dummy object around. It seems like a
not very common used Print family (not documented AFAICT) so maybe we
should remove it all instead.
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 |