diff options
| author | Pierre-Marie Pédrot | 2019-10-16 16:27:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-16 16:27:53 +0200 |
| commit | cc9856e33fa1a15fe699e8d9cd7b76086563683d (patch) | |
| tree | 3a51c6466ff40685d2c126a3997390c227b2ce8b /plugins | |
| parent | 5d82451d6d6f591ad81919d8e6529cee48474b9e (diff) | |
| parent | afd214869f050d07f9774d770c289bdc6e602dfd (diff) | |
Merge PR #10885: Remove [in_section] arguments to Safe_typing functions
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/table.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 96a3d00dc2..be9259861a 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -380,7 +380,7 @@ let check_inside_module () = warn_extraction_inside_module () let check_inside_section () = - if Lib.sections_are_opened () then + if Global.sections_are_opened () then err (str "You can't do that within a section." ++ fnl () ++ str "Close it and try again.") |