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.ml13
-rw-r--r--engine/evd.mli13
-rw-r--r--engine/namegen.ml2
-rw-r--r--engine/proofview.ml18
-rw-r--r--engine/termops.ml14
-rw-r--r--engine/termops.mli3
-rw-r--r--engine/uState.ml2
-rw-r--r--engine/univGen.ml6
-rw-r--r--engine/univGen.mli3
-rw-r--r--engine/univMinim.ml1
13 files changed, 75 insertions, 51 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 8e7d942c37..4bfa7c45e3 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -902,14 +902,14 @@ let make_nonalgebraic_variable evd u =
let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s =
with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s)
-let fresh_constant_instance ?loc env evd c =
- with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
+let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c =
+ with_context_set ?loc rigid evd (UnivGen.fresh_constant_instance env c)
-let fresh_inductive_instance ?loc env evd i =
- with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i)
+let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i =
+ with_context_set ?loc rigid evd (UnivGen.fresh_inductive_instance env i)
-let fresh_constructor_instance ?loc env evd c =
- with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
+let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c =
+ with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c)
let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
@@ -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 8843adc853..2c1194a5de 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -653,10 +653,14 @@ val update_sigma_env : evar_map -> env -> evar_map
(** Polymorphic universes *)
-val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t
-val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
-val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
-val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid
+ -> evar_map -> Sorts.family -> evar_map * Sorts.t
+val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid
+ -> env -> evar_map -> Constant.t -> evar_map * pconstant
+val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid
+ -> env -> evar_map -> inductive -> evar_map * pinductive
+val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid
+ -> env -> evar_map -> constructor -> evar_map * pconstructor
val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
evar_map -> GlobRef.t -> evar_map * econstr
@@ -707,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/proofview.ml b/engine/proofview.ml
index 16be96454e..b0ea75ac60 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -302,7 +302,8 @@ let tclONCE = Proof.once
exception MoreThanOneSuccess
let _ = CErrors.register_handler begin function
- | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.")
+ | MoreThanOneSuccess ->
+ Pp.str "This tactic has more than one success."
| _ -> raise CErrors.Unhandled
end
@@ -347,8 +348,7 @@ exception NoSuchGoals of int
let _ = CErrors.register_handler begin function
| NoSuchGoals n ->
- CErrors.user_err
- (str "No such " ++ str (String.plural n "goal") ++ str ".")
+ str "No such " ++ str (String.plural n "goal") ++ str "."
| _ -> raise CErrors.Unhandled
end
@@ -420,12 +420,9 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
exception SizeMismatch of int*int
let _ = CErrors.register_handler begin function
| SizeMismatch (i,j) ->
- let open Pp in
- let errmsg =
- str"Incorrect number of goals" ++ spc() ++
- str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
- in
- CErrors.user_err errmsg
+ let open Pp in
+ str"Incorrect number of goals" ++ spc() ++
+ str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
| _ -> raise CErrors.Unhandled
end
@@ -910,7 +907,8 @@ let tclPROGRESS t =
tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
let _ = CErrors.register_handler begin function
- | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+ | Logic_monad.Tac_Timeout ->
+ Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!"
| _ -> raise CErrors.Unhandled
end
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/univGen.ml b/engine/univGen.ml
index 1fe09270ba..b270f9dc0b 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -48,8 +48,6 @@ let fresh_instance_from ?loc ctx = function
(** Fresh universe polymorphic construction *)
-open Globnames
-
let fresh_global_instance ?loc ?names env gr =
let auctx = Environ.universes_of_global env gr in
let u, ctx = fresh_instance_from ?loc auctx names in
@@ -78,10 +76,6 @@ let constr_of_monomorphic_global gr =
Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
str " would forget universes.")
-let fresh_global_or_constr_instance env = function
- | IsConstr c -> c, ContextSet.empty
- | IsGlobal gr -> fresh_global_instance env gr
-
let fresh_sort_in_family = function
| InSProp -> Sorts.sprop, ContextSet.empty
| InProp -> Sorts.prop, ContextSet.empty
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 1b351c61c4..bbde9d4e30 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -46,9 +46,6 @@ val fresh_constructor_instance : env -> constructor ->
val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
constr in_universe_context_set
-val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
- constr in_universe_context_set
-
(** Get fresh variables for the universe context.
Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
val fresh_universe_context_set_instance : ContextSet.t ->
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-01 00:45:17 +0000