diff options
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 |