From 9e585d7479af0db837528a2fe2ce1690e22a36cb Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Sat, 16 Jan 2016 21:49:35 -0500 Subject: Universes algorithm : clarified comments --- kernel/univ.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/univ.ml') diff --git a/kernel/univ.ml b/kernel/univ.ml index fab0e6fb8..ebe3db0a3 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -12,8 +12,8 @@ (* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *) (* Support for universe polymorphism by MS [2014] *) -(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, - Pierre-Marie Pédrot *) +(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu + Sozeau, Pierre-Marie Pédrot *) open Pp open Errors -- cgit v1.2.3