Standardize constr -> globref operations to use destRef/isRef/isRefX

Instead of various termops and globnames aliases.

6 files changed, 28 insertions, 32 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8a650d9e7a..9ea2224272 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -90,14 +90,13 @@ let rec decompose_term env sigma t=
        if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found
 
 (* decompose equality in members and type *)
-open Termops
 
 let atom_of_constr env sigma term =
   let wh = whd_delta env sigma term in
   let kot = EConstr.kind sigma wh in
     match kot with
       App (f,args)->
-        if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
+        if isRefX sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
           then `Eq (args.(0),
                    decompose_term env sigma args.(1),
                    decompose_term env sigma args.(2))
@@ -132,7 +131,7 @@ let non_trivial = function
 let patterns_of_constr env sigma nrels term=
   let f,args=
     try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in
-        if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
+        if isRefX sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3
         then
           let patt1,rels1 = pattern_of_constr env sigma args.(1)
           and patt2,rels2 = pattern_of_constr env sigma args.(2) in
@@ -153,7 +152,7 @@ let patterns_of_constr env sigma nrels term=
 let rec quantified_atom_of_constr env sigma nrels term =
   match EConstr.kind sigma (whd_delta env sigma term) with
       Prod (id,atom,ff) ->
-        if is_global sigma (Lazy.force _False) ff then
+        if isRefX sigma (Lazy.force _False) ff then
           let patts=patterns_of_constr env sigma nrels atom in
               `Nrule patts
         else
@@ -165,7 +164,7 @@ let rec quantified_atom_of_constr env sigma nrels term =
 let litteral_of_constr env sigma term=
   match EConstr.kind sigma (whd_delta env sigma term) with
     | Prod (id,atom,ff) ->
-        if is_global sigma (Lazy.force _False) ff then
+        if isRefX sigma (Lazy.force _False) ff then
           match (atom_of_constr env sigma atom) with
               `Eq(t,a,b) -> `Neq(t,a,b)
             | `Other(p) -> `Nother(p)
@@ -517,7 +516,7 @@ let f_equal =
     in
     Proofview.tclORELSE
       begin match EConstr.kind sigma concl with
-      | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r ->
+      | App (r,[|_;t;t'|]) when isRefX sigma (Lazy.force _eq) r ->
           begin match EConstr.kind sigma t, EConstr.kind sigma t' with
           | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
               let rec cuts i =
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 =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a0eefd1a39..fbc64d95d0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -289,18 +289,18 @@ end) = struct
     if Int.equal n 0 then c
     else
       match EConstr.kind sigma c with
-      | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
+      | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f ->
         decomp_pointwise sigma (pred n) relb
-      | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
+      | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f ->
         decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1]))
       | _ -> invalid_arg "decomp_pointwise"
 
   let rec apply_pointwise sigma rel = function
     | arg :: args ->
       (match EConstr.kind sigma rel with
-      | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f ->
+      | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f ->
         apply_pointwise sigma relb args
-      | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f ->
+      | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f ->
         apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args
       | _ -> invalid_arg "apply_pointwise")
     | [] -> rel
@@ -357,7 +357,7 @@ end) = struct
     match EConstr.kind sigma t with
     | App (c, args) when Array.length args >= 2 ->
       let head = if isApp sigma c then fst (destApp sigma c) else c in
-        if Termops.is_global sigma (coq_eq_ref ()) head then None
+        if isRefX sigma (coq_eq_ref ()) head then None
         else
           (try
            let params, args = Array.chop (Array.length args - 2) args in
@@ -1880,13 +1880,13 @@ let declare_projection n instance_id r =
       let rec aux t =
         match EConstr.kind sigma t with
         | App (f, [| a ; a' ; rel; rel' |])
-            when Termops.is_global sigma (PropGlobal.respectful_ref ()) f ->
+            when isRefX sigma (PropGlobal.respectful_ref ()) f ->
           succ (aux rel')
         | _ -> 0
       in
       let init =
         match EConstr.kind sigma typ with
-            App (f, args) when Termops.is_global sigma (PropGlobal.respectful_ref ()) f  ->
+            App (f, args) when isRefX sigma (PropGlobal.respectful_ref ()) f  ->
               mkApp (f, fst (Array.chop (Array.length args - 2) args))
           | _ -> typ
       in aux init
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index a57cc76faa..de70fb292a 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -341,8 +341,8 @@ let coerce_to_reference sigma v =
   match Value.to_constr v with
   | Some c ->
     begin
-      try fst (Termops.global_of_constr sigma c)
-      with Not_found -> raise (CannotCoerceTo "a reference")
+      try fst (EConstr.destRef sigma c)
+      with DestKO -> raise (CannotCoerceTo "a reference")
     end
   | None -> raise (CannotCoerceTo "a reference")
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index f7e4a95a22..3841501b6a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -18,7 +18,6 @@ open EConstr
 open Vars
 open CClosure
 open Environ
-open Globnames
 open Glob_term
 open Locus
 open Tacexpr
@@ -43,12 +42,12 @@ type protection = Evd.evar_map -> EConstr.t -> GlobRef.t -> (Int.t -> protect_fl
 
 let global_head_of_constr sigma c =
   let f, args = decompose_app sigma c in
-    try fst (Termops.global_of_constr sigma f)
-    with Not_found -> CErrors.anomaly (str "global_head_of_constr.")
+    try fst (EConstr.destRef sigma f)
+    with DestKO -> CErrors.anomaly (str "global_head_of_constr.")
 
 let global_of_constr_nofail c =
-  try global_of_constr c
-  with Not_found -> GlobRef.VarRef (Id.of_string "dummy")
+  try fst @@ Constr.destRef c
+  with DestKO -> GlobRef.VarRef (Id.of_string "dummy")
 
 let rec mk_clos_but f_map n t =
   let (f, args) = Constr.decompose_appvect t in
@@ -97,9 +96,9 @@ let protect_tac_in map id =
 
 let rec closed_under sigma cset t =
   try
-    let (gr, _) = Termops.global_of_constr sigma t in
+    let (gr, _) = destRef sigma t in
     GlobRef.Set_env.mem gr cset
-  with Not_found ->
+  with DestKO ->
     match EConstr.kind sigma t with
     | Cast(c,_,_) -> closed_under sigma cset c
     | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
@@ -758,22 +757,21 @@ let af_ar = my_reference"AF_AR"
 let f_r = my_reference"F_R"
 let sf_sr = my_reference"SF_SR"
 let dest_field env evd th_spec =
-  let open Termops in
   let th_typ = Retyping.get_type_of env !evd th_spec in
   match EConstr.kind !evd th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when is_global !evd (Lazy.force afield_theory) f ->
+        when isRefX !evd (Lazy.force afield_theory) f ->
         let rth = plapp evd af_ar
           [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when is_global !evd (Lazy.force field_theory) f ->
+        when isRefX !evd (Lazy.force field_theory) f ->
         let rth =
           plapp evd f_r
             [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;div;inv;req|])
-        when is_global !evd (Lazy.force sfield_theory) f ->
+        when isRefX !evd (Lazy.force sfield_theory) f ->
         let rth = plapp evd sf_sr
           [|r;zero;one;add;mul;div;inv;req;th_spec|] in
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 6cb464918a..915531cf3c 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -34,7 +34,6 @@ open Tacinterp
 open Pretyping
 open Ppconstr
 open Printer
-open Globnames
 open Namegen
 open Evar_kinds
 open Constrexpr
@@ -464,7 +463,7 @@ let nb_cs_proj_args pc f u =
   | Sort s -> na (Sort_cs (Sorts.family s))
   | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f
   | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f
-  | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f))
+  | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f))
   | _ -> -1
   with Not_found -> -1