Merge branch 'located-universes'

8 files changed, 115 insertions, 90 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index f751f4d922..b6849f7ffb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -781,25 +781,25 @@ let restrict_universe_context evd vars =
 let universe_subst evd =
   UState.subst evd.universes
 
-let merge_context_set ?(sideff=false) rigid evd ctx' = 
-  {evd with universes = UState.merge sideff rigid evd.universes ctx'}
+let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
+  {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'}
 
 let merge_universe_subst evd subst = 
   {evd with universes = UState.merge_subst evd.universes subst }
 
-let with_context_set rigid d (a, ctx) = 
-  (merge_context_set rigid d ctx, a)
+let with_context_set ?loc rigid d (a, ctx) =
+  (merge_context_set ?loc rigid d ctx, a)
 
-let new_univ_level_variable ?name ?(predicative=true) rigid evd =
-  let uctx', u = UState.new_univ_variable rigid name evd.universes in
+let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd =
+  let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?name ?(predicative=true) rigid evd =
-  let uctx', u = UState.new_univ_variable rigid name evd.universes in
+let new_univ_variable ?loc ?name ?(predicative=true) rigid evd =
+  let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?name ?(predicative=true) rigid d =
-  let (d', u) = new_univ_variable rigid ?name ~predicative d in
+let new_sort_variable ?loc ?name ?(predicative=true) rigid d =
+  let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in
     (d', Type u)
 
 let add_global_univ d u =
@@ -815,27 +815,27 @@ let make_evar_universe_context e l =
   | Some us ->
       List.fold_left
         (fun uctx (loc,id) ->
-        fst (UState.new_univ_variable univ_rigid (Some (Id.to_string id)) uctx))
+        fst (UState.new_univ_variable ~loc univ_rigid (Some (Id.to_string id)) uctx))
         uctx us
 
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
 
-let fresh_sort_in_family ?(rigid=univ_flexible) env evd s = 
-  with_context_set rigid evd (Universes.fresh_sort_in_family env s)
+let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
+  with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s)
 
-let fresh_constant_instance env evd c =
-  with_context_set univ_flexible evd (Universes.fresh_constant_instance env c)
+let fresh_constant_instance ?loc env evd c =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c)
 
-let fresh_inductive_instance env evd i =
-  with_context_set univ_flexible evd (Universes.fresh_inductive_instance env i)
+let fresh_inductive_instance ?loc env evd i =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i)
 
-let fresh_constructor_instance env evd c =
-  with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
+let fresh_constructor_instance ?loc env evd c =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c)
 
-let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set rigid evd (Universes.fresh_global_instance ?names env gr)
+let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
+  with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr)
 
 let whd_sort_variable evd t = t
 
diff --git a/engine/evd.mli b/engine/evd.mli
index a9ca9a7408..3ae6e586c1 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -504,9 +504,9 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
 val normalize_evar_universe_context : evar_universe_context -> 
   evar_universe_context
 
-val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level
+val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe
+val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 											   
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
@@ -541,10 +541,10 @@ val universes : evar_map -> UGraph.t
 val merge_universe_context : evar_map -> evar_universe_context -> evar_map
 val set_universe_context : evar_map -> evar_universe_context -> evar_map
 
-val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map
+val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map
 val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
 
-val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
+val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
 
 val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
 val abstract_undefined_variables : evar_universe_context -> evar_universe_context
@@ -559,12 +559,12 @@ val update_sigma_env : evar_map -> env -> evar_map
 
 (** Polymorphic universes *)
 
-val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
-val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant
-val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive
-val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
+val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant
+val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
+val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
-val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> 
+val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> 
   Globnames.global_reference -> evar_map * constr
 
 (********************************************************************
diff --git a/engine/sigma.ml b/engine/sigma.ml
index c25aac0c14..c7b0bb5a50 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -36,36 +36,36 @@ let new_evar sigma ?naming info =
 let define evk c sigma =
   Sigma ((), Evd.define evk c sigma, ())
 
-let new_univ_level_variable ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in
+let new_univ_level_variable ?loc ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in
   Sigma (u, sigma, ())
 
-let new_univ_variable ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in
+let new_univ_variable ?loc ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in
   Sigma (u, sigma, ())
 
-let new_sort_variable ?name ?predicative rigid sigma =
-  let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in
+let new_sort_variable ?loc ?name ?predicative rigid sigma =
+  let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in
   Sigma (u, sigma, ())
 
-let fresh_sort_in_family ?rigid env sigma s =
-  let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in
+let fresh_sort_in_family ?loc ?rigid env sigma s =
+  let (sigma, s) = Evd.fresh_sort_in_family ?loc ?rigid env sigma s in
   Sigma (s, sigma, ())
 
-let fresh_constant_instance env sigma cst =
-  let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in
+let fresh_constant_instance ?loc env sigma cst =
+  let (sigma, cst) = Evd.fresh_constant_instance ?loc env sigma cst in
   Sigma (cst, sigma, ())
 
-let fresh_inductive_instance env sigma ind =
-  let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in
+let fresh_inductive_instance ?loc env sigma ind =
+  let (sigma, ind) = Evd.fresh_inductive_instance ?loc env sigma ind in
   Sigma (ind, sigma, ())
 
-let fresh_constructor_instance env sigma pc =
-  let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in
+let fresh_constructor_instance ?loc env sigma pc =
+  let (sigma, c) = Evd.fresh_constructor_instance ?loc env sigma pc in
   Sigma (c, sigma, ())
 
-let fresh_global ?rigid ?names env sigma r =
-  let (sigma, c) = Evd.fresh_global ?rigid ?names env sigma r in
+let fresh_global ?loc ?rigid ?names env sigma r =
+  let (sigma, c) = Evd.fresh_global ?loc ?rigid ?names env sigma r in
   Sigma (c, sigma, ())
 
 (** Run *)
diff --git a/engine/sigma.mli b/engine/sigma.mli
index d7ae2e4ac9..643bea4036 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -66,23 +66,23 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
 
 (** Polymorphic universes *)
 
-val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
-  'r t -> (Univ.universe_level, 'r) sigma
-val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
-  'r t -> (Univ.universe, 'r) sigma
-val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid ->
-  'r t -> (Sorts.t, 'r) sigma
-
-val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env ->
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+  Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma
+val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+  Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma
+val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
+  Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma
+
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env ->
   'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
 val fresh_constant_instance :
-  Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
+  ?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
 val fresh_inductive_instance :
-  Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
-val fresh_constructor_instance : Environ.env -> 'r t -> constructor ->
+  ?loc:Loc.t -> Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
+val fresh_constructor_instance : ?loc:Loc.t -> Environ.env -> 'r t -> constructor ->
   (pconstructor, 'r) sigma
 
-val fresh_global : ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
+val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
   'r t -> Globnames.global_reference -> (constr, 'r) sigma
 
 (** FILLME *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 75c03bc89c..8aa9a61ab9 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -25,9 +25,14 @@ module UNameMap = struct
         | _, _ -> r) s t
 end
 
+type uinfo = {
+  uname : string option;
+  uloc : Loc.t option;
+}
+
 (* 2nd part used to check consistency on the fly. *)
 type t =
- { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
+ { uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t;
    uctx_local : Univ.universe_context_set; (** The local context of variables *)
    uctx_univ_variables : Universes.universe_opt_subst;
    (** The local universes that are unification variables *)
@@ -104,8 +109,13 @@ let constrain_variables diff ctx =
       with Not_found | Option.IsNone -> cstrs)
     diff Univ.Constraint.empty
 
-let add_uctx_names s l (names, names_rev) =
-  (UNameMap.add s l names, Univ.LMap.add l s names_rev)
+let add_uctx_names ?loc s l (names, names_rev) =
+  (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev)
+
+let add_uctx_loc l loc (names, names_rev) =
+  match loc with
+  | None -> (names, names_rev)
+  | Some _ -> (names, Univ.LMap.add l { uname = None; uloc = loc } names_rev)
 
 let of_binders b =
   let ctx = empty in
@@ -230,8 +240,8 @@ let add_universe_constraints ctx cstrs =
 let pr_uctx_level uctx = 
   let map, map_rev = uctx.uctx_names in 
     fun l ->
-      try str(Univ.LMap.find l map_rev)
-      with Not_found -> 
+      try str (Option.get (Univ.LMap.find l map_rev).uname)
+      with Not_found | Option.IsNone ->
         Universes.pr_with_global_universes l
 
 let universe_context ?names ctx =
@@ -252,10 +262,14 @@ let universe_context ?names ctx =
      in
        if not (Univ.LSet.is_empty left) then
          let n = Univ.LSet.cardinal left in
-           errorlabstrm "universe_context"
+         let loc =
+          let get_loc u = try (Univ.LMap.find u (snd ctx.uctx_names)).uloc with Not_found -> None in
+          try List.find_map get_loc (Univ.LSet.elements left) with Not_found -> Loc.ghost
+         in
+           user_err_loc (loc, "universe_context",
                         (str(CString.plural n "Universe") ++ spc () ++
                              Univ.LSet.pr (pr_uctx_level ctx) left ++
-                             spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
+                             spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound."))
       else
         let inst = Univ.Instance.of_array (Array.of_list newinst) in
         let ctx = Univ.UContext.make (inst,
@@ -274,7 +288,7 @@ let univ_rigid = UnivRigid
 let univ_flexible = UnivFlexible false
 let univ_flexible_alg = UnivFlexible true
 
-let merge sideff rigid uctx ctx' =
+let merge ?loc sideff rigid uctx ctx' =
   let open Univ in
   let levels = ContextSet.levels ctx' in
   let uctx = if sideff then uctx else
@@ -301,10 +315,21 @@ let merge sideff rigid uctx ctx' =
                with UGraph.AlreadyDeclared when sideff -> g)
               levels g
   in
+  let uctx_names =
+    let fold u accu =
+      let modify _ info = match info.uloc with
+      | None -> { info with uloc = loc }
+      | Some _ -> info
+      in
+      try LMap.modify u modify accu
+      with Not_found -> LMap.add u { uname = None; uloc = loc } accu
+    in
+    (fst uctx.uctx_names, LSet.fold fold levels (snd uctx.uctx_names))
+  in
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare uctx.uctx_universes in
   let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
-    { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
+    { uctx with uctx_names; uctx_local; uctx_universes; uctx_initial_universes = initial }
 
 let merge_subst uctx s =
   { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
@@ -313,7 +338,7 @@ let emit_side_effects eff u =
   let uctxs = Safe_typing.universes_of_private eff in
   List.fold_left (merge true univ_rigid) u uctxs
 
-let new_univ_variable rigid name
+let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
   let ctx' = Univ.ContextSet.add_universe u ctx in
@@ -328,8 +353,8 @@ let new_univ_variable rigid name
   in
   let names = 
     match name with
-    | Some n -> add_uctx_names n u uctx.uctx_names
-    | None -> uctx.uctx_names
+    | Some n -> add_uctx_names ?loc n u uctx.uctx_names
+    | None -> add_uctx_loc u loc uctx.uctx_names
   in
   let initial =
     UGraph.add_universe u false uctx.uctx_initial_universes
diff --git a/engine/uState.mli b/engine/uState.mli
index 9dc96622ea..c5c454020c 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -84,11 +84,11 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-val merge : bool -> rigid -> t -> Univ.universe_context_set -> t
+val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t
 val merge_subst : t -> Universes.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
-val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
 val add_global_univ : t -> Univ.Level.t -> t
 val make_flexible_variable : t -> bool -> Univ.Level.t -> t
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5e8c5beb58..8329de2ee4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -143,12 +143,12 @@ let interp_universe_level_name evd (loc,s) =
 	  evd, Idmap.find id names
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
-  	    new_univ_level_variable ~name:s univ_rigid evd
+  	    new_univ_level_variable ~loc ~name:s univ_rigid evd
 	  else user_err_loc (loc, "interp_universe_level_name",
 			     Pp.(str "Undeclared universe: " ++ str s))
 
-let interp_universe evd = function
-  | [] -> let evd, l = new_univ_level_variable univ_rigid evd in
+let interp_universe ?loc evd = function
+  | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
 	    evd, Univ.Universe.make l
   | l ->
     List.fold_left (fun (evd, u) l -> 
@@ -156,15 +156,15 @@ let interp_universe evd = function
 	(evd', Univ.sup u (Univ.Universe.make l)))
     (evd, Univ.Universe.type0m) l
 
-let interp_universe_level evd = function
-  | None -> new_univ_level_variable univ_rigid evd
+let interp_universe_level loc evd = function
+  | None -> new_univ_level_variable ~loc univ_rigid evd
   | Some (loc,s) -> interp_universe_level_name evd (loc,s)
 
-let interp_sort evd = function
+let interp_sort ?loc evd = function
   | GProp -> evd, Prop Null
   | GSet -> evd, Prop Pos
   | GType n -> 
-    let evd, u = interp_universe evd n in
+    let evd, u = interp_universe ?loc evd n in
       evd, Type u
 
 let interp_elimination_sort = function
@@ -385,11 +385,11 @@ let evar_kind_of_term sigma c =
 (*************************************************************************)
 (* Main pretyping function                                               *)
 
-let interp_universe_level_name evd l =
+let interp_universe_level_name loc evd l =
   match l with
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
-  | GType s -> interp_universe_level evd s
+  | GType s -> interp_universe_level loc evd s
 
 let pretype_global loc rigid env evd gr us = 
   let evd, instance = 
@@ -404,7 +404,7 @@ let pretype_global loc rigid env evd gr us =
 		       str "Universe instance should have length " ++ int len)
        else
 	 let evd, l' = List.fold_left (fun (evd, univs) l -> 
-	    let evd, l = interp_universe_level_name evd l in
+	    let evd, l = interp_universe_level_name loc evd l in
 	      (evd, l :: univs)) (evd, []) l
 	 in
 	 if List.exists (fun l -> Univ.Level.is_prop l) l' then
@@ -413,7 +413,7 @@ let pretype_global loc rigid env evd gr us =
 		   str " universe instances must be greater or equal to Set.");
 	 evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
   in
-    Evd.fresh_global ~rigid ?names:instance env evd gr
+    Evd.fresh_global ~loc ~rigid ?names:instance env evd gr
 
 let pretype_ref loc evdref env ref us =
   match ref with
@@ -431,17 +431,17 @@ let pretype_ref loc evdref env ref us =
     let ty = Typing.unsafe_type_of env evd c in
       make_judge c ty
 
-let judge_of_Type evd s =
-  let evd, s = interp_universe evd s in
+let judge_of_Type loc evd s =
+  let evd, s = interp_universe ~loc evd s in
   let judge = 
     { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
   in
     evd, judge
 
-let pretype_sort evdref = function
+let pretype_sort loc evdref = function
   | GProp -> judge_of_prop
   | GSet -> judge_of_set
-  | GType s -> evd_comb1 judge_of_Type evdref s
+  | GType s -> evd_comb1 (judge_of_Type loc) evdref s
 
 let new_type_evar env evdref loc =
   let sigma = Sigma.Unsafe.of_evar_map !evdref in
@@ -598,7 +598,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
   | GSort (loc,s) ->
-    let j = pretype_sort evdref s in
+    let j = pretype_sort loc evdref s in
       inh_conv_coerce_to_tycon loc env evdref j tycon
 
   | GApp (loc,f,args) ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index bfb4e7325e..40745ed097 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -148,7 +148,7 @@ val ise_pretype_gen :
 
 (** To embed constr in glob_constr *)
 
-val interp_sort : evar_map -> glob_sort -> evar_map * sorts
+val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
 val interp_elimination_sort : glob_sort -> sorts_family
 
 val genarg_interp_hook :