From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 00:41:31 +0100
Subject: Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
---
 library/impargs.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 836568b890..a63264b669 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -228,10 +228,12 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all avoid na (_,b as envnames_b) =
+let find_displayed_name_in all avoid na (env, b) =
+  let b = EConstr.of_constr b in
+  let envnames_b = (env, b) in
   let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in flag avoid na b
-  else compute_displayed_name_in flag avoid na b
+  if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
+  else compute_displayed_name_in Evd.empty flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
-- 
cgit v1.2.3


From d6175b9980808ff91f1299ca26a9a49a117169ca Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Apr 2017 17:34:23 +0200
Subject: Fix a normalization hotspot in computation of constr keys.

Getting a key only needs to observe the root of a term. This hotspot was
observed in HoTT.
---
 library/keys.ml  | 4 ++--
 library/keys.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/keys.ml b/library/keys.ml
index 057dc3b65d..c9e325ee57 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -114,11 +114,11 @@ let inKeys : key_obj -> obj =
 let declare_equiv_keys ref ref' =
   Lib.add_anonymous_leaf (inKeys (ref,ref'))
 
-let constr_key c =
+let constr_key kind c =
   let open Globnames in 
   try 
     let rec aux k = 
-      match kind_of_term k with
+      match kind k with
       | Const (c, _) -> KGlob (ConstRef c)
       | Ind (i, u) -> KGlob (IndRef i)
       | Construct (c,u) -> KGlob (ConstructRef c)
diff --git a/library/keys.mli b/library/keys.mli
index 69668590d6..6abac4de44 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -16,7 +16,7 @@ val declare_equiv_keys : key -> key -> unit
 val equiv_keys : key -> key -> bool
 (** Check equivalence of keys. *)
 
-val constr_key : Term.constr -> key option
+val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
 (** Compute the head key of a term. *)
 
 val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds
-- 
cgit v1.2.3