aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-15 21:54:34 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-15 21:54:34 +0200
commit9beec0fc6cc283294bbbda363a3f788ae56347d5 (patch)
tree2df172ba10cedaa935460eed511a9dc494d1bafa /printing
parent5b109c098a46e5083ba0cf98b5fe72312331770e (diff)
parent63896b2443e71e47c016fc9d0709cc22cf24f288 (diff)
Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state
Diffstat (limited to 'printing')
-rw-r--r--printing/prettyp.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2b21b3f9e..3ae7da8fc 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -587,8 +587,6 @@ let gallina_print_library_entry with_values ent =
Some (str " >>>>>>> Module " ++ pr_name oname)
| (oname,Lib.ClosedModule _) ->
Some (str " >>>>>>> Closed Module " ++ pr_name oname)
- | (_,Lib.FrozenState _) ->
- None
let gallina_print_context with_values =
let rec prec n = function