aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml37
-rw-r--r--engine/eConstr.mli12
-rw-r--r--engine/evarutil.ml2
-rw-r--r--engine/evd.ml1
-rw-r--r--engine/evd.mli1
-rw-r--r--engine/namegen.ml2
-rw-r--r--engine/termops.ml14
-rw-r--r--engine/termops.mli3
-rw-r--r--engine/uState.ml2
-rw-r--r--engine/univMinim.ml1
10 files changed, 53 insertions, 22 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 150dad16c2..08e283f524 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,27 @@ 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
+
+(** Kind of type *)
+
+type kind_of_type =
+ | SortType of ESorts.t
+ | CastType of types * t
+ | ProdType of Name.t Context.binder_annot * t * t
+ | LetInType of Name.t Context.binder_annot * t * t * t
+ | AtomicType of t * t array
+
+let kind_of_type sigma t = match kind sigma t with
+ | Sort s -> SortType s
+ | Cast (c,_,t) -> CastType (c, t)
+ | Prod (na,t,c) -> ProdType (na, t, c)
+ | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
+ | App (c,l) -> AtomicType (c, l)
+ | (Rel _ | Meta _ | Var _ | Evar _ | Const _
+ | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
+ -> AtomicType (t,[||])
+ | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
module Unsafe =
struct
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 90f50b764c..ead7d88176 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -80,7 +80,14 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
val to_constr_opt : Evd.evar_map -> t -> Constr.t option
(** Same as [to_constr], but returns [None] if some unresolved evars remain *)
-val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
+type kind_of_type =
+ | SortType of ESorts.t
+ | CastType of types * t
+ | ProdType of Name.t Context.binder_annot * t * t
+ | LetInType of Name.t Context.binder_annot * t * t * t
+ | AtomicType of t * t array
+
+val kind_of_type : Evd.evar_map -> t -> kind_of_type
(** {5 Constructors} *)
@@ -152,6 +159,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 +183,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 +328,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/evd.ml b/engine/evd.ml
index 70f58163fd..4bfa7c45e3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1364,7 +1364,6 @@ module MiniEConstr = struct
let kind sigma c = Constr.kind (whd_evar sigma c)
let kind_upto = kind
- let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
let of_kind = Constr.of_kind
let of_constr c = c
let of_constr_array v = v
diff --git a/engine/evd.mli b/engine/evd.mli
index 82e1003a65..2c1194a5de 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -711,7 +711,6 @@ module MiniEConstr : sig
val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
- val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type
val whd_evar : evar_map -> t -> t
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 56277e8092..bcc8c34a4d 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -216,7 +216,6 @@ let it_mkLambda_or_LetIn_name env sigma b hyps =
let get_mangle_names =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"mangle auto-generated names"
~key:["Mangle";"Names"]
~value:false
@@ -227,7 +226,6 @@ let set_prefix x = mangle_names_prefix := forget_subscript x
let () = Goptions.(
declare_string_option
{ optdepr = false;
- optname = "mangled names prefix";
optkey = ["Mangle";"Names";"Prefix"];
optread = (fun () -> Id.to_string !mangle_names_prefix);
optwrite = begin fun x ->
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/engine/uState.ml b/engine/uState.ml
index 3546ece581..2eaa202246 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -53,7 +53,7 @@ let empty =
uctx_weak_constraints = UPairSet.empty; }
let elaboration_sprop_cumul =
- Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
+ Goptions.declare_bool_option_and_ref ~depr:false
~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
let make ~lbound u =
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index fc0770cf75..53ff041fa5 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -15,7 +15,6 @@ open UnivSubst
let get_set_minimization =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"minimization to Set"
~key:["Universe";"Minimization";"ToSet"]
~value:true
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:01:18 +0000