diff options
| author | Emilio Jesus Gallego Arias | 2020-06-03 16:34:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-03 17:33:25 +0200 |
| commit | 6fe12fdac4acee36c99ea780d260ce5a9756cb1d (patch) | |
| tree | 9e3016023ed13df51988a84e6f1f8b26d4b0584d /vernac/comAssumption.ml | |
| parent | 5ea6ef71681770a98edc5ede8614d2cf0bd48554 (diff) | |
[declare] Hide internals of variable declaration entries.
In particular this avoids exposing `Evd.side_effects proof_entry` in
the API.
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 023d76ce3b..44c30598aa 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -24,8 +24,7 @@ module RelDecl = Context.Rel.Declaration let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let kind = Decls.IsAssumption kind in - let decl = Declare.SectionLocalAssum {typ; impl} in - let () = Declare.declare_variable ~name ~kind decl in + let () = Declare.declare_variable ~name ~kind ~typ ~impl in let () = Declare.assumption_message name in let r = GlobRef.VarRef name in let () = maybe_declare_manual_implicits true r imps in |