diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-18 21:21:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-18 21:21:01 +0200 |
| commit | a7e66e4f3af85be7a4d345d0f8c6bde5a7a0c7b0 (patch) | |
| tree | c03ee45c7e0f7b6ed7bfd21c52b9e3295684490b /kernel/univ.ml | |
| parent | 892c74d099fd9eda1e2f179645f7e1d9b67ba49b (diff) | |
Clean a bit of univ.ml, add credits.
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index fd65d7de5..fed053d65 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 |