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 +-
 plugins/ltac/taccoerce.ml     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

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
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 95620b3747..b76009c997 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -255,7 +255,7 @@ let coerce_to_evaluable_ref env sigma v =
     | IndRef _ | ConstructRef _ -> fail ()
   else
     match Value.to_constr v with
-    | Some c when isConst sigma c -> EvalConstRef (Univ.out_punivs (destConst sigma c))
+    | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
     | Some c when isVar sigma c -> EvalVarRef (destVar sigma c)
     | _ -> fail ()
   in if Tacred.is_evaluable env ev then ev else fail ()
-- 
cgit v1.2.3