From b71e68fb78ccde52f1aaa63ef26f0135b92e9be5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Sep 2017 14:58:28 +0200
Subject: Parse directly to Sorts.family when appropriate.

When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
---
 pretyping/pretyping.ml  | 12 ------------
 pretyping/pretyping.mli |  4 ----
 2 files changed, 16 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 79d2c3333b..7cd35f530a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -222,18 +222,6 @@ let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
   | None -> new_univ_level_variable ?loc univ_rigid evd
   | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s)
 
-let interp_sort ?loc evd = function
-  | GProp -> evd, Prop Null
-  | GSet -> evd, Prop Pos
-  | GType n -> 
-    let evd, u = interp_universe ?loc evd n in
-      evd, Type u
-
-let interp_elimination_sort = function
-  | GProp -> InProp
-  | GSet  -> InSet
-  | GType _ -> InType
-
 type inference_hook = env -> evar_map -> evar -> evar_map * constr
 
 type inference_flags = {
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7395e94a09..5822f5add5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,7 +18,6 @@ open Evd
 open EConstr
 open Glob_term
 open Evarutil
-open Misctypes
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
@@ -119,9 +118,6 @@ val ise_pretype_gen :
 
 (** To embed constr in glob_constr *)
 
-val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
-val interp_elimination_sort : glob_sort -> sorts_family
-
 val register_constr_interp0 :
   ('r, 'g, 't) Genarg.genarg_type ->
     (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
-- 
cgit v1.2.3