diff options
| author |  Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2016-01-16 21:49:35 -0500 |
|---|---|---|
| committer |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-17 14:49:41 +0100 |
| commit | 9e585d7479af0db837528a2fe2ce1690e22a36cb (patch) | |
| tree | 4763680ec1fa387782cbd51941ba7f6c11664c7e /kernel/univ.ml | |
| parent | 820a282fde5cb4233116ce2cda927fda2f36097d (diff) | |
Universes algorithm : clarified comments
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |