From 7c82718f18afa3b317873f756a8801774ef64061 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:19:20 +0200
Subject: Minor typo in universe polymorphism doc.

---
 dev/doc/univpoly.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

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
-- 
cgit v1.2.3


From c47b205206d832430fa80a3386be80149e281d33 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:04:56 +0200
Subject: Code cleaning in VM (with Benjamin).

Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
---
 dev/vm_printers.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

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;
-- 
cgit v1.2.3