From 470943bdf917caf352b5347c8d33fc39699805b0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Nov 2018 12:55:46 +0100
Subject: Fix mod_subst wrt universe polymorphism

---
 kernel/constr.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8e5d15dd2d..d67d15b23b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1361,7 +1361,7 @@ type rel_context = rel_declaration list
 type named_context = named_declaration list
 type compacted_context = compacted_declaration list
 
-(* Sorts and sort family *)
+(** Minimalistic constr printer, typically for debugging *)
 
 let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) =
   let open Pp in
@@ -1377,8 +1377,6 @@ let pr_puniverses p u =
   if Univ.Instance.is_empty u then p
   else Pp.(p ++ str"(*" ++ Univ.Instance.pr Univ.Level.pr u ++ str"*)")
 
-(* Minimalistic constr printer, typically for debugging *)
-
 let rec debug_print c =
   let open Pp in
   match kind c with
-- 
cgit v1.2.3