From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 23:20:25 +0200
Subject: Actually exporting delayed universes in the EConstr implementation.

For now we only normalize sorts, and we leave instances for the next
commit.
---
 plugins/ltac/rewrite.ml    | 2 +-
 plugins/ltac/taccoerce.ml  | 2 +-
 plugins/omega/coq_omega.ml | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 55172cba6a..b84be4600c 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -434,7 +434,7 @@ module TypeGlobal = struct
 end
 
 let sort_of_rel env evm rel =
-  Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel)
+  ESorts.kind evm (Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel))
 
 let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 114b8dda04..95620b3747 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -164,7 +164,7 @@ let id_of_name = function
 	  basename
        | Sort s ->
 	  begin
-	    match s with
+	    match ESorts.kind sigma s with
 	    | Prop _ -> Label.to_id (Label.make "Prop")
 	    | Type _ -> Label.to_id (Label.make "Type")
 	  end
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index adf9269587..a2016cb038 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1714,7 +1714,7 @@ let onClearedName2 id tac =
     end })
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
-  | Sort (Prop Null) -> true
+  | Sort s -> Sorts.is_prop (ESorts.kind sigma s)
   | Cast (c,_,_) -> is_Prop sigma c
   | _ -> false
 
-- 
cgit v1.2.3