diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-15 21:54:34 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-15 21:54:34 +0200 |
| commit | 9beec0fc6cc283294bbbda363a3f788ae56347d5 (patch) | |
| tree | 2df172ba10cedaa935460eed511a9dc494d1bafa /vernac | |
| parent | 5b109c098a46e5083ba0cf98b5fe72312331770e (diff) | |
| parent | 63896b2443e71e47c016fc9d0709cc22cf24f288 (diff) | |
Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6714b98f5..d0f9c7de7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -628,8 +628,7 @@ let vernac_constraint loc poly l = (* Modules *) let vernac_import export refl = - Library.import_module export (List.map qualid_of_reference refl); - Lib.add_frozen_state () + Library.import_module export (List.map qualid_of_reference refl) let vernac_declare_module export (loc, id) binders_ast mty_ast = (* We check the state of the system (in section, in module type) |