From a5f9b0ea89c9a595ce47c549a2ebb976b0ac3aa2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 7 Feb 2020 14:01:56 +0100
Subject: Standardize constr -> globref operations to use destRef/isRef/isRefX

Instead of various termops and globnames aliases.
---
 plugins/firstorder/sequent.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 65af123d9c..c77ddeb040 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -209,11 +209,11 @@ let extend_with_auto_hints env sigma l seq =
     | Res_pf (c,_) | Give_exact (c,_)
     | Res_pf_THEN_trivial_fail (c,_) ->
       let (c, _, _) = c in
-      (try
-         let (gr, _) = Termops.global_of_constr sigma c in
+      (match  EConstr.destRef sigma c with
+       | exception Constr.DestKO -> seq, sigma
+       | gr, _ ->
          let sigma, typ = Typing.type_of env sigma c in
-         add_formula env sigma Hint gr typ seq, sigma
-       with Not_found -> seq, sigma)
+         add_formula env sigma Hint gr typ seq, sigma)
     | _ -> seq, sigma
   in
   let h acc dbname =
-- 
cgit v1.2.3