aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml3
-rw-r--r--pretyping/cases.ml3
-rw-r--r--pretyping/classops.ml9
-rw-r--r--pretyping/evarconv.ml12
-rw-r--r--pretyping/evarconv.mli9
-rw-r--r--pretyping/evarsolve.ml5
-rw-r--r--pretyping/evarsolve.mli3
-rw-r--r--pretyping/heads.ml3
-rw-r--r--pretyping/indrec.ml8
-rw-r--r--pretyping/inductiveops.ml4
-rw-r--r--pretyping/inductiveops.mli8
-rw-r--r--pretyping/recordops.ml10
-rw-r--r--pretyping/reductionops.ml7
-rw-r--r--pretyping/typeclasses.ml30
-rw-r--r--pretyping/typing.ml12
-rw-r--r--pretyping/typing.mli10
16 files changed, 30 insertions, 106 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index b8958ca944..3da1ab7439 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -46,10 +46,9 @@ let discharge_rename_args = function
| _, (ReqGlobal (c, names), _ as req) ->
(try
let vars = Lib.variable_section_segment_of_reference c in
- let c' = pop_global_reference c in
let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
let names' = var_names @ names in
- Some (ReqGlobal (c', names), (c', names'))
+ Some (ReqGlobal (c, names), (c, names'))
with Not_found -> Some req)
| _ -> None
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2c821c96ba..9fa8442f8a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1713,7 +1713,8 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
let vl = List.map pi1 good in
let ty =
let ty = get_type_of !!env sigma t in
- Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty
+ let sigma, res = refresh_universes (Some false) !!env !evdref ty in
+ evdref := sigma; res
in
let dummy_subst = List.init k (fun _ -> mkProp) in
let ty = substl dummy_subst (aux x ty) in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b264e31474..b026397abf 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -451,12 +451,6 @@ let subst_coercion (subst, c) =
else { c with coercion_type = coe; coercion_source = cls;
coercion_target = clt; coercion_is_proj = clp; }
-let discharge_cl = function
- | CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
- | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
- | CL_PROJ p -> CL_PROJ (Lib.discharge_proj_repr p)
- | cl -> cl
-
let discharge_coercion (_, c) =
if c.coercion_local then None
else
@@ -467,9 +461,6 @@ let discharge_coercion (_, c) =
with Not_found -> 0
in
let nc = { c with
- coercion_type = Lib.discharge_global c.coercion_type;
- coercion_source = discharge_cl c.coercion_source;
- coercion_target = discharge_cl c.coercion_target;
coercion_params = n + c.coercion_params;
coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
} in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e978adf761..bae13dbba1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1386,8 +1386,6 @@ let solve_unif_constraints_with_heuristics env
check_problems_are_solved env heuristic_solved_evd;
solve_unconstrained_impossible_cases env heuristic_solved_evd
-let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics
-
(* Main entry points *)
exception UnableToUnify of evar_map * unification_error
@@ -1414,13 +1412,3 @@ let conv env ?(ts=default_transparent_state env) evd t1 t2 =
let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
make_opt(evar_conv_x ts env evd CUMUL t1 t2)
-
-let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 =
- match evar_conv_x ts env !evdref CONV t1 t2 with
- | Success evd' -> evdref := evd'; true
- | _ -> false
-
-let e_cumul env ?(ts=default_transparent_state env) evdref t1 t2 =
- match evar_conv_x ts env !evdref CUMUL t1 t2 with
- | Success evd' -> evdref := evd'; true
- | _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index cdf5dd0e50..20a4f34ec7 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -27,12 +27,6 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma
(** The same function resolving evars by side-effect and
catching the exception *)
-val e_conv : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
-[@@ocaml.deprecated "Use [Evarconv.conv]"]
-
-val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
-[@@ocaml.deprecated "Use [Evarconv.cumul]"]
-
val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
@@ -43,9 +37,6 @@ val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar
val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
-val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
-[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"]
-
(** Check all pending unification problems are solved and raise an
error otherwise *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 2dd3721980..44bfe4b6cc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -46,7 +46,8 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
(* direction: true for fresh universes lower than the existing ones *)
let refresh_sort status ~direction s =
let s = ESorts.kind !evdref s in
- let s' = evd_comb0 (new_sort_variable status) evdref in
+ let sigma, s' = new_sort_variable status !evdref in
+ evdref := sigma;
let evd =
if direction then set_leq_sort env !evdref s' s
else set_leq_sort env !evdref s s'
@@ -1690,8 +1691,6 @@ let reconsider_unif_constraints conv_algo evd =
(Success evd)
pbs
-let reconsider_conv_pbs = reconsider_unif_constraints
-
(* Tries to solve problem t1 = t2.
* Precondition: t1 is an uninstantiated evar
* Returns an optional list of evars that were instantiated, or None
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 3f05c58c41..4665ed29a2 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -62,9 +62,6 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
-val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
-[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"]
-
val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
constr -> alias list option
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 7d9debce34..a3e4eb8971 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -14,7 +14,6 @@ open Constr
open Vars
open Mod_subst
open Environ
-open Globnames
open Libobject
open Lib
open Context.Named.Declaration
@@ -171,7 +170,7 @@ let subst_head (subst,(ref,k)) =
let discharge_head (_,(ref,k)) =
match ref with
- | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
+ | EvalConstRef cst -> Some (ref, k)
| EvalVarRef id -> None
let rebuild_head (ref,k) =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 418fdf2a26..e49ba75b3f 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -455,8 +455,8 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
| ((indi,u),_,_,dep,kinds)::rest ->
let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel i lnamesparrec) in
let s =
- Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg)
- evdref kinds
+ let sigma, res = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg !evdref kinds in
+ evdref := sigma; res
in
let typP = make_arity env !evdref dep indf s in
let typP = EConstr.Unsafe.to_constr typP in
@@ -601,13 +601,13 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
let lookup_eliminator ind_sp s =
let kn,i = ind_sp in
- let mp,dp,l = KerName.repr (MutInd.canonical kn) in
+ let mp,l = KerName.repr (MutInd.canonical kn) in
let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
let id = add_suffix ind_id (elimination_suffix s) in
(* Try first to get an eliminator defined in the same section as the *)
(* inductive type *)
try
- let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in
+ let cst =Global.constant_of_delta_kn (KerName.make mp (Label.of_id id)) in
let _ = Global.lookup_constant cst in
ConstRef cst
with Not_found ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 0fa573b9a6..ea222397a8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -269,10 +269,6 @@ let allowed_sorts env (kn,i as ind) =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
mip.mind_kelim
-let projection_nparams_env _ p = Projection.npars p
-
-let projection_nparams p = Projection.npars p
-
let has_dependent_elim mib =
match mib.mind_record with
| PrimRecord _ -> mib.mind_finite == BiFinite
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index ea34707bfc..b2e205115f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -129,15 +129,9 @@ val allowed_sorts : env -> inductive -> Sorts.family list
val has_dependent_elim : mutual_inductive_body -> bool
(** Primitive projections *)
-val projection_nparams : Projection.t -> int
-[@@ocaml.deprecated "Use [Projection.npars]"]
-val projection_nparams_env : env -> Projection.t -> int
-[@@ocaml.deprecated "Use [Projection.npars]"]
-
val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
EConstr.t -> EConstr.types -> types
-
(** Extract information from an inductive family *)
type constructor_summary = {
@@ -152,8 +146,6 @@ val get_constructor :
pinductive * mutual_inductive_body * one_inductive_body * constr list ->
int -> constructor_summary
val get_constructors : env -> inductive_family -> constructor_summary array
-val get_projections : env -> inductive -> Projection.Repr.t array option
-[@@ocaml.deprecated "Use [Environ.get_projections]"]
(** [get_arity] returns the arity of the inductive family instantiated
with the parameters; if recursively non-uniform parameters are not
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c25416405e..3719f9302a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -79,12 +79,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
if projs' == projs && kn' == kn && id' == id then obj else
((kn',i),id',kl,projs')
-let discharge_constructor (ind, n) =
- (Lib.discharge_inductive ind, n)
-
-let discharge_structure (_,(ind,id,kl,projs)) =
- Some (Lib.discharge_inductive ind, discharge_constructor id, kl,
- List.map (Option.map Lib.discharge_con) projs)
+let discharge_structure (_,x) = Some x
let inStruc : struc_tuple -> obj =
declare_object {(default_object "STRUCTURE") with
@@ -319,8 +314,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) =
let ind' = subst_ind subst ind in
if cst' == cst && ind' == ind then obj else (cst',ind')
-let discharge_canonical_structure (_,(cst,ind)) =
- Some (Lib.discharge_con cst,Lib.discharge_inductive ind)
+let discharge_canonical_structure (_,x) = Some x
let inCanonStruc : Constant.t * inductive -> obj =
declare_object {(default_object "CANONICAL-STRUCTURE") with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e8c3b3e2b3..5dbe95a471 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -132,8 +132,7 @@ module ReductionBehaviour = struct
{ b with b_nargs = nargs'; b_recargs = recargs' }
else b
in
- let c = Lib.discharge_con c in
- Some (ReqGlobal (ConstRef c, req), (ConstRef c, b))
+ Some (ReqGlobal (gr, req), (ConstRef c, b))
| _ -> None
let rebuild = function
@@ -713,8 +712,8 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
| Name.Name id ->
let open UnivProblem in
try
- let (cst_mod,cst_sect,_) = Constant.repr3 reference in
- let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
+ let (cst_mod,_) = Constant.repr2 reference in
+ let cst = Constant.make2 cst_mod (Label.of_id id) in
let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
match constant_opt_value_in env (cst,u) with
| None -> bd
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 67c5643459..7e5815acd1 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -222,26 +222,26 @@ let discharge_class (_,cl) =
| Some (_, ((tc,_), _)) -> Some tc.cl_impl)
ctx'
in
- List.Smart.map (Option.Smart.map Lib.discharge_global) grs
- @ newgrs
+ grs @ newgrs
in grs', discharge_rel_context subst 1 ctx @ ctx' in
- let cl_impl' = Lib.discharge_global cl.cl_impl in
- if cl_impl' == cl.cl_impl then cl else
+ try
let info = abs_context cl in
let ctx = info.Lib.abstr_ctx in
let ctx, subst = rel_of_variable_context ctx in
let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
let context = discharge_context ctx (subst, usubst) cl.cl_context in
let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
- let discharge_proj (x, y, z) = x, y, Option.Smart.map Lib.discharge_con z in
- { cl_univs = cl_univs';
- cl_impl = cl_impl';
- cl_context = context;
- cl_props = props;
- cl_projs = List.Smart.map discharge_proj cl.cl_projs;
- cl_strict = cl.cl_strict;
- cl_unique = cl.cl_unique
- }
+ let discharge_proj x = x in
+ { cl_univs = cl_univs';
+ cl_impl = cl.cl_impl;
+ cl_context = context;
+ cl_props = props;
+ cl_projs = List.Smart.map discharge_proj cl.cl_projs;
+ cl_strict = cl.cl_strict;
+ cl_unique = cl.cl_unique
+ }
+ with Not_found -> (* not defined in the current section *)
+ cl
let rebuild_class cl =
try
@@ -365,8 +365,8 @@ let discharge_instance (_, (action, inst)) =
Some (action,
{ inst with
is_global = Some (pred n);
- is_class = Lib.discharge_global inst.is_class;
- is_impl = Lib.discharge_global inst.is_impl })
+ is_class = inst.is_class;
+ is_impl = inst.is_impl })
let is_local i = (i.is_global == None)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 4ba715f0d5..dc3f042431 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -398,9 +398,6 @@ let check env sigma c t =
error_actual_type_core env sigma j t
| Some sigma -> sigma
-let e_check env evdref c t =
- evdref := check env !evdref c t
-
(* Type of a constr *)
let unsafe_type_of env sigma c =
@@ -416,9 +413,6 @@ let sort_of env sigma c =
let sigma, a = type_judgment env sigma j in
sigma, a.utj_type
-let e_sort_of env evdref c =
- Evarutil.evd_comb1 (sort_of env) evdref c
-
(* Try to solve the existential variables by typing *)
let type_of ?(refresh=false) env sigma c =
@@ -429,16 +423,10 @@ let type_of ?(refresh=false) env sigma c =
Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma j.uj_type
else sigma, j.uj_type
-let e_type_of ?refresh env evdref c =
- Evarutil.evd_comb1 (type_of ?refresh env) evdref c
-
let solve_evars env sigma c =
let env = enrich_env env sigma in
let sigma, j = execute env sigma c in
(* side-effect on evdref *)
sigma, nf_evar sigma j.uj_val
-let e_solve_evars env evdref c =
- Evarutil.evd_comb1 (solve_evars env) evdref c
-
let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 3cf43ace01..b8830ff4a2 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -24,27 +24,17 @@ val unsafe_type_of : env -> evar_map -> constr -> types
universes *)
val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
-(** Variant of [type_of] using references instead of state-passing. *)
-val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
-[@@ocaml.deprecated "Use [Typing.type_of]"]
-
(** Typecheck a type and return its sort *)
val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
-val e_sort_of : env -> evar_map ref -> types -> Sorts.t
-[@@ocaml.deprecated "Use [Typing.sort_of]"]
(** Typecheck a term has a given type (assuming the type is OK) *)
val check : env -> evar_map -> constr -> types -> evar_map
-val e_check : env -> evar_map ref -> constr -> types -> unit
-[@@ocaml.deprecated "Use [Typing.check]"]
(** Returns the instantiated type of a metavariable *)
val meta_type : evar_map -> metavariable -> types
(** Solve existential variables using typing *)
val solve_evars : env -> evar_map -> constr -> evar_map * constr
-val e_solve_evars : env -> evar_map ref -> constr -> constr
-[@@ocaml.deprecated "Use [Typing.solve_evars]"]
(** Raise an error message if incorrect elimination for this inductive *)
(** (first constr is term to match, second is return predicate) *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:45:34 +0000