From 237b569dd6539fc1730dbd1dda29f83e24ef8d0c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 17 Jan 2015 20:17:17 +0530
Subject: Univs: proper printing of global and local universe names (only
 printing functions touched in the kernel).

---
 interp/constrextern.ml  | 2 +-
 interp/constrextern.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4b20b024dd..58e1eb1d17 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -956,7 +956,7 @@ let extern_type goal_concl_style env sigma t =
   let r = Detyping.detype goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
 
-let extern_sort s = extern_glob_sort (detype_sort s)
+let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
 
 let extern_closed_glob ?lax goal_concl_style env sigma t =
   let avoid = if goal_concl_style then ids_of_context env else [] in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index d11248a595..b797e455c0 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -40,7 +40,7 @@ val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
-val extern_sort : sorts -> glob_sort
+val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder list
 
-- 
cgit v1.2.3