diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-09 13:19:20 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-09 17:40:56 +0200 |
| commit | 7c82718f18afa3b317873f756a8801774ef64061 (patch) | |
| tree | 3b5b7be2a9ba5985775e247c15b5be70e872f0a9 /dev | |
| parent | 5e1296a5cae4ae0ab84ddbe7b0ec71959861af97 (diff) | |
Minor typo in universe polymorphism doc.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/univpoly.txt | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt index bad2ae36e..9e243eead 100644 --- a/dev/doc/univpoly.txt +++ b/dev/doc/univpoly.txt @@ -82,7 +82,7 @@ show that A's type is in cumululativity relation with id's type argument, incurring a universe constraint. To do this, one can simply call Typing.resolve_evars env evdref c which will do some infer_conv to produce the right constraints and put them in the evar_map. Of course in -some cases you might now from an invariant that no new constraint would +some cases you might know from an invariant that no new constraint would be produced and get rid of it. Anyway the kernel will tell you if you forgot some. As a temporary way out, [Universes.constr_of_global] allows you to make a constr from any non-polymorphic constant, but it will fail |