From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 13 Oct 2015 18:30:47 +0200
Subject: Fix some typos.

---
 dev/doc/univpoly.txt      | 2 +-
 dev/v8-syntax/memo-v8.tex | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index 9e243eead5..6a69c57934 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -167,7 +167,7 @@ kernel/univ.ml was modified. The new API forces every universe to be
 declared before it is mentionned in any constraint. This forces to
 declare every universe to be >= Set or > Set. Every universe variable
 introduced during elaboration is >= Set. Every _global_ universe is now
-declared explicitely > Set, _after_ typechecking the definition. In
+declared explicitly > Set, _after_ typechecking the definition. In
 polymorphic definitions Type@{i} ranges over Set and any other universe
 j. However, at instantiation time for polymorphic references, one can
 try to instantiate a universe parameter with Prop as well, if the
diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex
index 8d116de26f..ae4b569b36 100644
--- a/dev/v8-syntax/memo-v8.tex
+++ b/dev/v8-syntax/memo-v8.tex
@@ -253,7 +253,7 @@ became \TERM{context}. Syntax is unified with subterm matching.
 \subsection{Occurrences}
 
 To avoid ambiguity between a numeric literal and the optionnal
-occurence numbers of this term, the occurence numbers are put after
+occurrence numbers of this term, the occurrence numbers are put after
 the term itself. This applies to tactic \TERM{pattern} and also
 \TERM{unfold}
 \begin{transbox}
-- 
cgit v1.2.3


From a895b2c0caf8ec9c0deb04b8dea890283bd7329d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Oct 2015 12:16:36 +0200
Subject: Fixing  perfomance issue of auto hints induced by universes.

Instead of brutally merging the whole evarmap coming from the clenv,
we remember the context associated to the hint and we only merge that tiny
part of constraints. We need to be careful for polymorphic hints though,
as we have to refresh them beforehand.
---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f9f2e1b09e..059c812ad5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -165,7 +165,7 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
+let ppevm evd = pp(Evd.pr_evar_universe_context (Evd.evar_universe_context evd))
 let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
-- 
cgit v1.2.3


From 1d6c4f135d42a008b21d86d8ecd8b329405d8d7c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Oct 2015 18:51:47 +0200
Subject: Reverting modifications in dev/top_printers pushed mistakenly.

---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 059c812ad5..f9f2e1b09e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -165,7 +165,7 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(Evd.pr_evar_universe_context (Evd.evar_universe_context evd))
+let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
 let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
-- 
cgit v1.2.3