From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 02:36:16 +0200
Subject: Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
---
 plugins/ltac/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/extratactics.ml4')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 55108631bd..b34afd51bd 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1073,7 +1073,7 @@ let decompose l c =
   Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let to_ind c =
-      if isInd sigma c then Univ.out_punivs (destInd sigma c)
+      if isInd sigma c then fst (destInd sigma c)
       else error "not an inductive type"
     in
     let l = List.map to_ind l 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.
---
 plugins/ltac/extratactics.ml4 | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac/extratactics.ml4')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b34afd51bd..1ec52718a5 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1087,10 +1087,14 @@ END
 (** library/keys *)
 
 VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
-| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ 
-  let it c = EConstr.Unsafe.to_constr (snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c)) in 
-  let k1 = Keys.constr_key (it c) in
-  let k2 = Keys.constr_key (it c') in
+| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
+  let get_key c =
+    let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in
+    let kind c = EConstr.kind evd c in
+    Keys.constr_key kind c
+  in
+  let k1 = get_key c in
+  let k2 = get_key c' in
     match k1, k2 with
     | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2
     | _ -> () ]
-- 
cgit v1.2.3