From 22014c3fd400446556d3c2d7548d4638a7ed96ee Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 29 May 2017 17:39:03 +0200
Subject: Ltac cleanup: no more constr_of_global calls

---
 plugins/ltac/tacsubst.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/ltac/tacsubst.ml')

diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 4390ff08b..8cbe9c690 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,6 @@ open Stdarg
 open Tacarg
 open Misctypes
 open Globnames
-open Term
 open Genredexpr
 open Patternops
 
@@ -91,7 +90,7 @@ open Printer
 let subst_global_reference subst =
  let subst_global ref =
   let ref',t' = subst_global subst ref in
-   if not (eq_constr (Universes.constr_of_global ref') t') then
+   if not (is_global ref' t') then
     Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
           str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
           pr_global ref') ;
-- 
cgit v1.2.3