Simplify vars_of_global usage

11 files changed, 42 insertions, 33 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8ab3ce821e..cefffb315e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -166,6 +166,13 @@ let destProj sigma c = match kind sigma c with
 | Proj (p, c) -> (p, c)
 | _ -> raise DestKO
 
+let destRef sigma c = let open GlobRef in match kind sigma c with
+  | Var x -> VarRef x, EInstance.empty
+  | Const (c,u) -> ConstRef c, u
+  | Ind (ind,u) -> IndRef ind, u
+  | Construct (c,u) -> ConstructRef c, u
+  | _ -> raise DestKO
+
 let decompose_app sigma c =
   match kind sigma c with
     | App (f,cl) -> (f, Array.to_list cl)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f897448557..e27eecc24f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -180,6 +180,8 @@ val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
 
+val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
+
 val decompose_app : Evd.evar_map -> t -> t * t list
 
 (** Pops lambda abstractions until there are no more, skipping casts. *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 13356627f0..f9d9ce3569 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -549,7 +549,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
             if Id.Set.mem id' ids then
               raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
           in
-          Id.Set.iter check (Environ.vars_of_global env c)
+          Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c))
         in
         c
 
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
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 64e3977d68..f7b9469ae8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -118,7 +118,9 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
 val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
+
 val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
+[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
 
 (* Substitution of metavariables *)
 type meta_value_map = (metavariable * Constr.constr) list
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 7ffde3107b..b490aa5092 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -407,6 +407,12 @@ let destCoFix c = match kind c with
   | CoFix cofix -> cofix
   | _ -> raise DestKO
 
+let destRef c = let open GlobRef in match kind c with
+  | Var x -> VarRef x, Univ.Instance.empty
+  | Const (c,u) -> ConstRef c, u
+  | Ind (ind,u) -> IndRef ind, u
+  | Construct (c,u) -> ConstructRef c, u
+  | _ -> raise DestKO
 
 (******************************************************************)
 (* Flattening and unflattening of embedded applications and casts *)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 12819ac39d..c012f04260 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -343,6 +343,8 @@ val destFix : constr -> fixpoint
 
 val destCoFix : constr -> cofixpoint
 
+val destRef : constr -> GlobRef.t Univ.puniverses
+
 (** {6 Equality} *)
 
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 757c8773b7..3b7e3ae544 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -560,26 +560,22 @@ let universes_of_global env r =
 
 (* Returns the list of global variables in a term *)
 
-let vars_of_global env constr =
-  match kind constr with
-      Var id -> Id.Set.singleton id
-    | Const (kn, _) -> lookup_constant_variables kn env
-    | Ind (ind, _) -> lookup_inductive_variables ind env
-    | Construct (cstr, _) -> lookup_constructor_variables cstr env
-    (** FIXME: is Proj missing? *)
-    | _ -> raise Not_found
+let vars_of_global env gr =
+  let open GlobRef in
+  match gr with
+  | VarRef id -> Id.Set.singleton id
+  | ConstRef kn -> lookup_constant_variables kn env
+  | IndRef ind -> lookup_inductive_variables ind env
+  | ConstructRef cstr -> lookup_constructor_variables cstr env
 
 let global_vars_set env constr =
   let rec filtrec acc c =
-    let acc =
-      match kind c with
-      | Var _ | Const _ | Ind _ | Construct _ ->
-	  Id.Set.union (vars_of_global env c) acc
-      | _ ->
-	  acc in
-    Constr.fold filtrec acc c
+    match destRef c with
+    | gr, _ ->
+      Id.Set.union (vars_of_global env gr) acc
+    | exception DestKO -> Constr.fold filtrec acc c
   in
-    filtrec Id.Set.empty constr
+  filtrec Id.Set.empty constr
 
 
 (* [keep_hyps env ids] keeps the part of the section context of [env] which
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6e313faab0..3d653bcfe0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -276,8 +276,7 @@ val universes_of_global : env -> GlobRef.t -> AUContext.t
 
 val global_vars_set : env -> constr -> Id.Set.t
 
-(** the constr must be a global reference *)
-val vars_of_global : env -> constr -> Id.Set.t
+val vars_of_global : env -> GlobRef.t -> Id.Set.t
 
 (** closure of the input id set w.r.t. dependency *)
 val really_needed : env -> Id.Set.t -> Id.Set.t
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 62d719034c..22f438c00c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -457,7 +457,7 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
-        acc2 := Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) !acc2
+        acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2
     | _ ->
         iter_with_full_binders sigma
           (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 245bdce5ad..0c10f32c86 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -787,7 +787,7 @@ let secvars_of_constr env sigma c =
   secvars_of_idset (Termops.global_vars_set env sigma c)
 
 let secvars_of_global env gr =
-  secvars_of_idset (vars_of_global_reference env gr)
+  secvars_of_idset (vars_of_global env gr)
 
 let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env sigma c in