diff options
| author | Pierre-Marie Pédrot | 2015-10-10 12:24:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-10 12:24:28 +0200 |
| commit | 75c5e421e91d49eec9cd55c222595d2ef45325d6 (patch) | |
| tree | eac436f0dda95d74cc1cbe2676a32a760cb53c71 /dev | |
| parent | eb7da0d0a02a406c196214ec9d08384385541788 (diff) | |
| parent | db06a1ddee4c79ea8f6903596284df2f2700ddac (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/univpoly.txt | 2 | ||||
| -rw-r--r-- | dev/vm_printers.ml | 1 |
2 files changed, 1 insertions, 2 deletions
diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt index bad2ae36eb..9e243eead5 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 diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 3d688011c2..802b0f9d80 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -61,7 +61,6 @@ and ppstack s = and ppatom a = match a with | Aid idk -> print_idkey idk - | Aiddef(idk,_) -> print_string "&";print_idkey idk | Aind((sp,i),_) -> print_string "Ind("; print_string (string_of_mind sp); print_string ","; print_int i; |