From a7e66e4f3af85be7a4d345d0f8c6bde5a7a0c7b0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 18 Sep 2014 21:21:01 +0200
Subject: Clean a bit of univ.ml, add credits.

---
 kernel/univ.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index fd65d7de50..fed053d655 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -10,8 +10,10 @@
 (* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *)
 (* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *)
 (* 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 *)
+(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, 
+   Pierre-Marie Pédrot *)
 
 open Pp
 open Errors
@@ -153,9 +155,6 @@ module HList = struct
     
   let tip e = Node.make (Cons(e, nil))
 
-  (* let cons ?(sorted=true) e l = *)
-  (*   if sorted then sorted_cons e l else cons e l *)
-
   let fold f l acc =
     let rec loop acc l = match l.Hcons.node with
       | Nil -> acc
-- 
cgit v1.2.3