From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias 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. --- plugins/firstorder/rules.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder/rules.mli') diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index d8d4c1a38..5c46f4cec 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term -open EConstr open Names +open Constr +open EConstr open Globnames type tactic = unit Proofview.tactic -- cgit v1.2.3