aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/prettyp.ml')
-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