diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index c7c0766587..61321cd605 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -584,7 +584,7 @@ let declare_univ_binders gr pl = Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) let do_universe ~poly l = - let in_section = Lib.sections_are_opened () in + let in_section = Global.sections_are_opened () in let () = if poly && not in_section then CErrors.user_err ~hdr:"Constraint" |