aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/dischargedhypsmap.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/dischargedhypsmap.mli')
-rw-r--r--library/dischargedhypsmap.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index b264c1228..98e3d93d5 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -13,7 +13,6 @@ open Nametab
type discharged_hyps = full_path list
-(** {6 Sect } *)
(** Discharged hypothesis. Here we store the discharged hypothesis of each
constant or inductive type declaration. *)