From 78e600ac5f8aa9609cac4347c7a694428ae9d7cc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Oct 2020 14:06:12 +0100
Subject: Moving interpretation of user-level universes in constrintern.ml.

---
 interp/constrexpr_ops.mli | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'interp/constrexpr_ops.mli')

diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index edf52c93e8..dfa51918d1 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -123,10 +123,3 @@ val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -
 
 (** For cases pattern parsing errors *)
 val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
-
-(** Local universe and constraint declarations. *)
-val interp_univ_decl : Environ.env -> universe_decl_expr ->
-                       Evd.evar_map * UState.universe_decl
-
-val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
-                       Evd.evar_map * UState.universe_decl
-- 
cgit v1.2.3