aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/eConstr.ml17
-rw-r--r--engine/eConstr.mli3
-rw-r--r--engine/evarutil.ml2
-rw-r--r--engine/termops.ml14
-rw-r--r--engine/termops.mli3
-rw-r--r--interp/reserve.ml4
-rw-r--r--kernel/constr.ml15
-rw-r--r--kernel/constr.mli2
-rw-r--r--library/globnames.ml8
-rw-r--r--library/globnames.mli2
-rw-r--r--plugins/cc/cctac.ml11
-rw-r--r--plugins/firstorder/sequent.ml8
-rw-r--r--plugins/ltac/rewrite.ml14
-rw-r--r--plugins/ltac/taccoerce.ml4
-rw-r--r--plugins/setoid_ring/newring.ml20
-rw-r--r--plugins/ssrmatching/ssrmatching.ml3
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/recordops.ml4
-rw-r--r--pretyping/tacred.ml8
-rw-r--r--pretyping/typeclasses.ml12
-rw-r--r--tactics/equality.ml12
-rw-r--r--tactics/hipattern.ml8
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tactics.ml8
24 files changed, 100 insertions, 86 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 150dad16c2..e37a58be61 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -119,6 +119,20 @@ let isVarId sigma id c =
let isRelN sigma n c =
match kind sigma c with Rel n' -> Int.equal n n' | _ -> false
+let isRef sigma c = match kind sigma c with
+ | Const _ | Ind _ | Construct _ | Var _ -> true
+ | _ -> false
+
+let isRefX sigma x c =
+ let open GlobRef in
+ match x, kind sigma c with
+ | ConstRef c, Const (c', _) -> Constant.equal c c'
+ | IndRef i, Ind (i', _) -> eq_ind i i'
+ | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+ | VarRef id, Var id' -> Id.equal id id'
+ | _ -> false
+
+
let destRel sigma c = match kind sigma c with
| Rel p -> p
| _ -> raise DestKO
@@ -723,8 +737,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
evd, t
-let is_global sigma gr c =
- Globnames.is_global gr (to_constr sigma c)
+let is_global = isRefX
module Unsafe =
struct
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 90f50b764c..181714460d 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -152,6 +152,7 @@ val mkNamedProd_or_LetIn : named_declaration -> types -> types
val isRel : Evd.evar_map -> t -> bool
val isVar : Evd.evar_map -> t -> bool
val isInd : Evd.evar_map -> t -> bool
+val isRef : Evd.evar_map -> t -> bool
val isEvar : Evd.evar_map -> t -> bool
val isMeta : Evd.evar_map -> t -> bool
val isSort : Evd.evar_map -> t -> bool
@@ -175,6 +176,7 @@ val isArity : Evd.evar_map -> t -> bool
val isVarId : Evd.evar_map -> Id.t -> t -> bool
val isRelN : Evd.evar_map -> int -> t -> bool
+val isRefX : Evd.evar_map -> GlobRef.t -> t -> bool
val destRel : Evd.evar_map -> t -> int
val destMeta : Evd.evar_map -> t -> metavariable
@@ -319,6 +321,7 @@ val fresh_global :
Evd.evar_map -> GlobRef.t -> Evd.evar_map * t
val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
+[@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
(** {5 Extra} *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b09cc87f97..8533e05d3e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -555,7 +555,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
let () = if global then
let check id' =
if Id.Set.mem id' ids then
- raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
+ raise (ClearDependencyError (id',err,Some (fst @@ destRef c)))
in
Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c))
in
diff --git a/engine/termops.ml b/engine/termops.ml
index a65b8275e6..a5c179bf78 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1066,19 +1066,9 @@ let global_of_constr sigma c =
| Var id -> VarRef id, EConstr.EInstance.empty
| _ -> raise Not_found
-let is_global sigma c t =
- let open GlobRef in
- match c, EConstr.kind sigma t with
- | ConstRef c, Const (c', _) -> Constant.equal c c'
- | IndRef i, Ind (i', _) -> eq_ind i i'
- | ConstructRef i, Construct (i', _) -> eq_constructor i i'
- | VarRef id, Var id' -> Id.equal id id'
- | _ -> false
+let is_global = EConstr.isRefX
-let isGlobalRef sigma c =
- match EConstr.kind sigma c with
- | Const _ | Ind _ | Construct _ | Var _ -> true
- | _ -> false
+let isGlobalRef = EConstr.isRef
let is_template_polymorphic_ind env sigma f =
match EConstr.kind sigma f with
diff --git a/engine/termops.mli b/engine/termops.mli
index f970b9ece0..7bbf87239d 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -264,10 +264,13 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.
val is_section_variable : Id.t -> bool
val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t
+[@@ocaml.deprecated "Use [EConstr.destRef] instead (throws DestKO instead of Not_found)."]
val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
+[@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
val isGlobalRef : Evd.evar_map -> constr -> bool
+[@@ocaml.deprecated "Use [EConstr.isRef] instead."]
val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool
diff --git a/interp/reserve.ml b/interp/reserve.ml
index e81439c3d5..4a731e57a3 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -104,8 +104,8 @@ let declare_reserved_type idl t =
let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table
let constr_key c =
- try RefKey (canonical_gr (global_of_constr (fst (Constr.decompose_app c))))
- with Not_found -> Oth
+ try RefKey (canonical_gr (fst @@ Constr.destRef (fst (Constr.decompose_app c))))
+ with Constr.DestKO -> Oth
let revert_reserved_type t =
try
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 15e5c512ed..84eacb196c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -253,7 +253,7 @@ let mkFloat f = Float f
least one argument and the function is not itself an applicative
term *)
-let kind c = c
+let kind (c:t) = c
let rec kind_nocast_gen kind c =
match kind c with
@@ -338,6 +338,19 @@ let isProj c = match kind c with Proj _ -> true | _ -> false
let isFix c = match kind c with Fix _ -> true | _ -> false
let isCoFix c = match kind c with CoFix _ -> true | _ -> false
+let isRef c = match kind c with
+ | Const _ | Ind _ | Construct _ | Var _ -> true
+ | _ -> false
+
+let isRefX x c =
+ let open GlobRef in
+ match x, kind c with
+ | ConstRef c, Const (c', _) -> Constant.equal c c'
+ | IndRef i, Ind (i', _) -> eq_ind i i'
+ | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+ | VarRef id, Var id' -> Id.equal id id'
+ | _ -> false
+
(* Destructs a de Bruijn index *)
let destRel c = match kind c with
| Rel n -> n
diff --git a/kernel/constr.mli b/kernel/constr.mli
index d4af1149c2..159570b5ea 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -256,6 +256,8 @@ val isRel : constr -> bool
val isRelN : int -> constr -> bool
val isVar : constr -> bool
val isVarId : Id.t -> constr -> bool
+val isRef : constr -> bool
+val isRefX : GlobRef.t -> constr -> bool
val isInd : constr -> bool
val isEvar : constr -> bool
val isMeta : constr -> bool
diff --git a/library/globnames.ml b/library/globnames.ml
index 63cb2c69bd..e55a7b5499 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -73,13 +73,7 @@ let global_of_constr c = match kind c with
| Var id -> VarRef id
| _ -> raise Not_found
-let is_global c t =
- match c, kind t with
- | ConstRef c, Const (c', _) -> Constant.equal c c'
- | IndRef i, Ind (i', _) -> eq_ind i i'
- | ConstructRef i, Construct (i', _) -> eq_constructor i i'
- | VarRef id, Var id' -> Id.equal id id'
- | _ -> false
+let is_global = Constr.isRefX
let printable_constr_of_global = function
| VarRef id -> mkVar id
diff --git a/library/globnames.mli b/library/globnames.mli
index d61cdd2b64..fb59cbea4e 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -32,6 +32,7 @@ val destIndRef : GlobRef.t -> inductive
val destConstructRef : GlobRef.t -> constructor
val is_global : GlobRef.t -> constr -> bool
+[@@ocaml.deprecated "Use [Constr.isRefX] instead."]
val subst_constructor : substitution -> constructor -> constructor
val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
@@ -44,6 +45,7 @@ val printable_constr_of_global : GlobRef.t -> constr
(** Turn a construction denoting a global reference into a global reference;
raise [Not_found] if not a global reference *)
val global_of_constr : constr -> GlobRef.t
+[@@ocaml.deprecated "Use [Constr.destRef] instead (throws DestKO instead of Not_found)."]
(** {6 Extended global references } *)
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
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3bd52088c7..c21af82659 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -269,7 +269,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
let sk2 = Stack.append_app args sk2 in
lookup_canonical_conversion (proji, Const_cs c2), sk2
| _ ->
- let (c2, _) = Termops.global_of_constr sigma t2 in
+ let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
lookup_canonical_conversion (proji, Const_cs c2),sk2
with Not_found ->
let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3b918b5396..879c007198 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -189,7 +189,7 @@ let rec cs_pattern_of_constr env t =
let _, params = Inductive.find_rectype env ty in
Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
| Sort s -> Sort_cs (Sorts.family s), None, []
- | _ -> Const_cs (Globnames.global_of_constr t) , None, []
+ | _ -> Const_cs (fst @@ destRef t) , None, []
let warn_projection_no_head_constant =
CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
@@ -234,7 +234,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
((GlobRef.ConstRef proji_sp, (patt, t)),
{ o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
:: acc
- | exception Not_found ->
+ | exception DestKO ->
if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
acc
) acc spopt
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f87c50b5e4..4afed07eda 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1311,11 +1311,9 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else
error_cannot_recognize ref
| _ ->
- try
- if GlobRef.equal (fst (global_of_constr sigma c)) ref
- then it_mkProd_or_LetIn t l
- else raise Not_found
- with Not_found ->
+ if isRefX sigma ref c
+ then it_mkProd_or_LetIn t l
+ else
try
let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in
elimrec env t' l
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1541e96635..d5c8c3bd19 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -107,9 +107,9 @@ let class_info env sigma c =
not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c))
let global_class_of_constr env sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.find gr !classes, u
- with Not_found -> not_a_class env sigma c
+ with DestKO | Not_found -> not_a_class env sigma c
let dest_class_app env sigma c =
let cl, args = EConstr.decompose_app sigma c in
@@ -125,9 +125,9 @@ let class_of_constr env sigma c =
with e when CErrors.noncritical e -> None
let is_class_constr sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.mem gr !classes
- with Not_found -> false
+ with DestKO | Not_found -> false
let rec is_class_type evd c =
let c, _ = Termops.decompose_app_vect evd c in
@@ -140,9 +140,9 @@ let is_class_evar evd evi =
is_class_type evd evi.Evd.evar_concl
let is_class_constr sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.mem gr !classes
- with Not_found -> false
+ with DestKO | Not_found -> false
let rec is_maybe_class_type evd c =
let c, _ = Termops.decompose_app_vect evd c in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9195746dc6..9ef5f478d3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
Proofview.Goal.enter_one begin fun gl ->
let sigma = project gl in
let is_global_exists gr c =
- Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c
+ Coqlib.has_ref gr && isRefX sigma (Coqlib.lib_ref gr) c
in
let inccl = Option.is_empty cls in
let env = Proofview.Goal.env gl in
@@ -1339,11 +1339,11 @@ let inject_if_homogenous_dependent_pair ty =
let existTconstr = Coqlib.lib_ref "core.sigT.intro" in
(* check whether the equality deals with dep pairs or not *)
let eqTypeDest = fst (decompose_app sigma t) in
- if not (Termops.is_global sigma sigTconstr eqTypeDest) then raise Exit;
+ if not (isRefX sigma sigTconstr eqTypeDest) then raise Exit;
let hd1,ar1 = decompose_app_vect sigma t1 and
hd2,ar2 = decompose_app_vect sigma t2 in
- if not (Termops.is_global sigma existTconstr hd1) then raise Exit;
- if not (Termops.is_global sigma existTconstr hd2) then raise Exit;
+ if not (isRefX sigma existTconstr hd1) then raise Exit;
+ if not (isRefX sigma existTconstr hd2) then raise Exit;
let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
(* check if the user has declared the dec principle *)
(* and compare the fst arguments of the dep pair *)
@@ -1692,8 +1692,8 @@ let () =
optwrite = (:=) regular_subst_tactic }
let restrict_to_eq_and_identity eq = (* compatibility *)
- if not (is_global (lib_ref "core.eq.type") eq) &&
- not (is_global (lib_ref "core.identity.type") eq)
+ if not (Constr.isRefX (lib_ref "core.eq.type") eq) &&
+ not (Constr.isRefX (lib_ref "core.identity.type") eq)
then raise Constr_matching.PatternMatchingFailure
exception FoundHyp of (Id.t * constr * bool)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index c5ed02e043..5404404af5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -431,10 +431,10 @@ let match_eq sigma eqn (ref, hetero) =
in
match EConstr.kind sigma eqn with
| App (c, [|t; x; y|]) ->
- if not hetero && Termops.is_global sigma ref c then PolymorphicLeibnizEq (t, x, y)
+ if not hetero && isRefX sigma ref c then PolymorphicLeibnizEq (t, x, y)
else raise PatternMatchingFailure
| App (c, [|t; x; t'; x'|]) ->
- if hetero && Termops.is_global sigma ref c then HeterogenousEq (t, x, t', x')
+ if hetero && isRefX sigma ref c then HeterogenousEq (t, x, t', x')
else raise PatternMatchingFailure
| _ -> raise PatternMatchingFailure
@@ -479,9 +479,9 @@ let find_this_eq_data_decompose env sigma eqn =
let match_sigma env sigma ex =
match EConstr.kind sigma ex with
- | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sig.intro") f ->
+ | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sig.intro") f ->
build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr)
- | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f ->
+ | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sigT.intro") f ->
build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
| _ -> raise PatternMatchingFailure
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 2181eb25af..4239fc8bc0 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -352,7 +352,7 @@ let dest_nf_eq env sigma t = match EConstr.kind sigma t with
| App (r, [| t; x; y |]) ->
let open Reductionops in
let eq = Coqlib.lib_ref "core.eq.type" in
- if EConstr.is_global sigma eq r then
+ if isRefX sigma eq r then
(t, whd_all env sigma x, whd_all env sigma y)
else user_err Pp.(str "Not an equality.")
| _ ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 609b752716..2d900a237a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3955,7 +3955,7 @@ let specialize_eqs id =
match EConstr.kind !evars ty with
| Prod (na, t, b) ->
(match EConstr.kind !evars t with
- | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq ->
+ | App (eq, [| eqty; x; y |]) when isRefX !evars Coqlib.(lib_ref "core.eq.type") eq ->
let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
let pt = mkApp (eq, [| eqty; c; c |]) in
let ind = destInd !evars eq in
@@ -3963,7 +3963,7 @@ let specialize_eqs id =
if unif (push_rel_context ctx env) evars pt t then
aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
else acc, in_eqs, ctx, ty
- | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq ->
+ | App (heq, [| eqty; x; eqty'; y |]) when isRefX !evars (Lazy.force coq_heq_ref) heq ->
let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in
let pt = mkApp (heq, [| eqt; c; eqt; c |]) in
let ind = destInd !evars heq in
@@ -4134,8 +4134,8 @@ let compute_elim_sig sigma ?elimc elimt =
| Some (LocalDef _) -> error_ind_scheme ""
| Some (LocalAssum (_,ind)) ->
let indhd,indargs = decompose_app sigma ind in
- try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) }
- with e when CErrors.noncritical e ->
+ try {!res with indref = Some (fst (destRef sigma indhd)) }
+ with DestKO ->
error "Cannot find the inductive type of the inductive scheme."
let compute_scheme_signature evd scheme names_info ind_type_guess =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:08:51 +0000