From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 6 Nov 2017 23:27:09 +0100
Subject: [api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.
---
 tactics/autorewrite.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics/autorewrite.ml')

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ed612c0fc..e68087f14 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -10,6 +10,7 @@ open Equality
 open Names
 open Pp
 open Term
+open Constr
 open Termops
 open CErrors
 open Util
@@ -20,7 +21,7 @@ open Locus
 type rew_rule = { rew_lemma: constr;
 		  rew_type: types;
 		  rew_pat: constr;
-		  rew_ctx: Univ.universe_context_set;
+		  rew_ctx: Univ.ContextSet.t;
 		  rew_l2r: bool;
 		  rew_tac: Genarg.glob_generic_argument option }
 
-- 
cgit v1.2.3