From 30a2f4c5469e25038f5720f03e948519efeef48d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 7 Feb 2020 13:54:23 +0100
Subject: ReferenceVariables error contains a globref instead of a constr

The previous system was from before globref was in the kernel.
---
 vernac/himsg.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 17c3e0395a..dfc4631572 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -201,9 +201,7 @@ let explain_bad_assumption env sigma j =
   str "because this term is not a type."
 
 let explain_reference_variables sigma id c =
-  (* c is intended to be a global reference *)
-  let pc = pr_global (fst (Termops.global_of_constr sigma c)) in
-  pc ++ strbrk " depends on the variable " ++ Id.print id ++
+  pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++
   strbrk " which is not declared in the context."
 
 let rec pr_disjunction pr = function
-- 
cgit v1.2.3