From 9f47342d890dc3ef7f4950004513a47d940af5ca Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Nov 2017 03:09:43 +0100
Subject: [api] A few more minor deprecation notices.

Note the problem with `create_evar_defs`.
---
 pretyping/cases.mli     | 4 ++--
 pretyping/pretyping.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 3a139b7b03..43dbc31058 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -13,8 +13,8 @@ open Environ
 open EConstr
 open Inductiveops
 open Glob_term
-open Evarutil
 open Ltac_pretype
+open Evardefine
 
 (** {5 Compilation of pattern-matching } *)
 
@@ -116,7 +116,7 @@ type 'a pattern_matching_problem =
 val compile : 'a pattern_matching_problem -> unsafe_judgment
 
 val prepare_predicate : ?loc:Loc.t ->
-           (Evarutil.type_constraint ->
+           (type_constraint ->
             Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index eb2b435bf6..b2735ee22c 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -17,8 +17,8 @@ open Environ
 open Evd
 open EConstr
 open Glob_term
-open Evarutil
 open Ltac_pretype
+open Evardefine
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
-- 
cgit v1.2.3