From 5993c266300cca1c7ca6e8b2b8e3f77f745ca9f9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 13:27:27 +0200
Subject: Simplify vars_of_global usage

---
 engine/termops.ml | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 1244074d50..ee0c3d210e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -912,9 +912,9 @@ let occur_in_global env id constr =
 
 let occur_var env sigma id c =
   let rec occur_rec c =
-    match EConstr.kind sigma c with
-    | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c)
-    | _ -> EConstr.iter sigma occur_rec c
+    match EConstr.destRef sigma c with
+    | gr, _ -> occur_in_global env id gr
+    | exception DestKO -> EConstr.iter sigma occur_rec c
   in
   try occur_rec c; false with Occur -> true
 
@@ -961,9 +961,7 @@ let collect_vars sigma c =
   | _ -> EConstr.fold sigma aux vars c in
   aux Id.Set.empty c
 
-let vars_of_global_reference env gr =
-  let c, _ = Global.constr_of_global_in_context env gr in
-  vars_of_global env c
+let vars_of_global_reference = vars_of_global
 
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
@@ -1458,12 +1456,9 @@ let clear_named_body id env =
 
 let global_vars_set env sigma constr =
   let rec filtrec acc c =
-    let acc = match EConstr.kind sigma c with
-    | Var _ | Const _ | Ind _ | Construct _ ->
-      Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
-    | _ -> acc
-    in
-    EConstr.fold sigma filtrec acc c
+    match EConstr.destRef sigma c with
+    | gr, _ -> Id.Set.union (vars_of_global env gr) acc
+    | exception DestKO -> EConstr.fold sigma filtrec acc c
   in
   filtrec Id.Set.empty constr
 
-- 
cgit v1.2.3