aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml33
-rw-r--r--engine/evarutil.mli9
-rw-r--r--engine/evd.ml58
-rw-r--r--engine/evd.mli14
-rw-r--r--engine/ftactic.ml7
-rw-r--r--engine/ftactic.mli3
-rw-r--r--engine/proofview.ml15
-rw-r--r--engine/proofview.mli6
-rw-r--r--engine/termops.ml20
-rw-r--r--engine/termops.mli24
-rw-r--r--engine/uState.ml4
-rw-r--r--engine/uState.mli3
-rw-r--r--engine/univGen.ml42
-rw-r--r--engine/univGen.mli27
-rw-r--r--engine/univMinim.ml2
15 files changed, 49 insertions, 218 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 96beb72a56..0a5bba39b9 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -26,24 +26,7 @@ let safe_evar_value sigma ev =
try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev)
with NotInstantiatedEvar | Not_found -> None
-(** Combinators *)
-
-let evd_comb0 f evdref =
- let (evd',x) = f !evdref in
- evdref := evd';
- x
-
-let evd_comb1 f evdref x =
- let (evd',y) = f !evdref x in
- evdref := evd';
- y
-
-let evd_comb2 f evdref x y =
- let (evd',z) = f !evdref x y in
- evdref := evd';
- z
-
-let new_global evd x =
+let new_global evd x =
let (evd, c) = Evd.fresh_global (Global.env()) evd x in
(evd, c)
@@ -673,26 +656,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids =
(* spiwack: a few functions to gather evars on which goals depend. *)
let queue_set q is_dependent set =
Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
-let queue_term q is_dependent c =
- queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c))
+let queue_term evm q is_dependent c =
+ queue_set q is_dependent (evars_of_term evm c)
let process_dependent_evar q acc evm is_dependent e =
let evi = Evd.find evm e in
(* Queues evars appearing in the types of the goal (conclusion, then
hypotheses), they are all dependent. *)
- queue_term q true evi.evar_concl;
+ queue_term evm q true evi.evar_concl;
List.iter begin fun decl ->
let open NamedDecl in
- queue_term q true (NamedDecl.get_type decl);
+ queue_term evm q true (NamedDecl.get_type decl);
match decl with
| LocalAssum _ -> ()
- | LocalDef (_,b,_) -> queue_term q true b
+ | LocalDef (_,b,_) -> queue_term evm q true b
end (EConstr.named_context_of_val evi.evar_hyps);
match evi.evar_body with
| Evar_empty ->
if is_dependent then Evar.Map.add e None acc else acc
| Evar_defined b ->
- let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in
+ let subevars = evars_of_term evm b in
(* evars appearing in the definition of an evar [e] are marked
as dependent when [e] is dependent itself: if [e] is a
non-dependent goal, then, unless they are reach from another
@@ -812,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi =
in
let accu = match evi.evar_body with
| Evar_empty -> Evar.Set.empty
- | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b)
+ | Evar_defined b -> evars_of_term sigma b
in
let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in
let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index bb0da44103..8eaff8bd13 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -274,15 +274,6 @@ val push_rel_context_to_named_context : ?hypnaming:naming_mode ->
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
-(** Evar combinators *)
-
-val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
-[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
-
val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
Evar_kinds.t Loc.located
diff --git a/engine/evd.ml b/engine/evd.ml
index b89222cf8e..15b4c31851 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -222,7 +222,7 @@ let map_evar_body f = function
let map_evar_info f evi =
{evi with
evar_body = map_evar_body f evi.evar_body;
- evar_hyps = map_named_val f evi.evar_hyps;
+ evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps;
evar_concl = f evi.evar_concl;
evar_candidates = Option.map (List.map f) evi.evar_candidates }
@@ -823,33 +823,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
| Evar (evk2,_) -> fst (evar_source evk2 evd)
| _ -> None
-(** The following functions return the set of evars immediately
- contained in the object *)
-
-(* excluding defined evars *)
-
-let evars_of_term c =
- let rec evrec acc c =
- match kind c with
- | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
- | _ -> Constr.fold evrec acc c
- in
- evrec Evar.Set.empty c
-
-let evars_of_named_context nc =
- Context.Named.fold_outside
- (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr)))
- nc
- ~init:Evar.Set.empty
-
-let evars_of_filtered_evar_info evi =
- Evar.Set.union (evars_of_term evi.evar_concl)
- (Evar.Set.union
- (match evi.evar_body with
- | Evar_empty -> Evar.Set.empty
- | Evar_defined b -> evars_of_term b)
- (evars_of_named_context (evar_filtered_context evi)))
-
(**********************************************************)
(* Sort variables *)
@@ -869,8 +842,6 @@ let to_universe_context evd = UState.context evd.universes
let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
-let const_univ_entry = univ_entry
-
let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
let restrict_universe_context evd vars =
@@ -1406,3 +1377,30 @@ module MiniEConstr = struct
let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
end
+
+(** The following functions return the set of evars immediately
+ contained in the object *)
+
+(* excluding defined evars *)
+
+let evars_of_term evd c =
+ let rec evrec acc c =
+ match MiniEConstr.kind evd c with
+ | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
+ | _ -> Constr.fold evrec acc c
+ in
+ evrec Evar.Set.empty c
+
+let evars_of_named_context evd nc =
+ Context.Named.fold_outside
+ (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr)))
+ nc
+ ~init:Evar.Set.empty
+
+let evars_of_filtered_evar_info evd evi =
+ Evar.Set.union (evars_of_term evd evi.evar_concl)
+ (Evar.Set.union
+ (match evi.evar_body with
+ | Evar_empty -> Evar.Set.empty
+ | Evar_defined b -> evars_of_term evd b)
+ (evars_of_named_context evd (evar_filtered_context evi)))
diff --git a/engine/evd.mli b/engine/evd.mli
index b0fcddb068..587a1de044 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -491,16 +491,15 @@ val extract_changed_conv_pbs : evar_map ->
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option
-(** The following functions return the set of evars immediately
- contained in the object; need the term to be evar-normal otherwise
- defined evars are returned too. *)
+(** The following functions return the set of undefined evars
+ contained in the object. *)
-val evars_of_term : constr -> Evar.Set.t
+val evars_of_term : evar_map -> econstr -> Evar.Set.t
(** including evars in instances of evars *)
-val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t
+val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
-val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
+val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
(** Metas *)
val meta_list : evar_map -> (metavariable * clbinding) list
@@ -615,9 +614,6 @@ val to_universe_context : evar_map -> Univ.UContext.t
val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
val merge_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index ac0344148a..dab2e7d5ef 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -56,13 +56,6 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
-let nf_enter f =
- bind goals
- (fun gl ->
- gl >>= fun gl ->
- Proofview.Goal.normalize gl >>= fun nfgl ->
- Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"]
-
let enter f =
bind goals
(fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 3c4fa6f4e8..ed95d62bc6 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -41,9 +41,6 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
(** {5 Focussing} *)
-val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
-[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
-
(** Enter a goal. The resulting tactic is focussed. *)
val enter : (Proofview.Goal.t -> 'a t) -> 'a t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index f278c83912..5c5a02d3fa 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -46,7 +46,7 @@ let compact el ({ solution } as pv) =
let apply_subst_einfo _ ei =
Evd.({ ei with
evar_concl = nf ei.evar_concl;
- evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+ evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps;
evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
@@ -641,7 +641,7 @@ let shelve_goals l =
[sigma]. *)
let depends_on sigma src tgt =
let evi = Evd.find sigma tgt in
- Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi))
+ Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi))
let unifiable_delayed g l =
CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l
@@ -1104,13 +1104,6 @@ module Goal = struct
tclZERO ~info e
end
end
-
- let normalize { self; state } =
- Env.get >>= fun env ->
- tclEVARMAP >>= fun sigma ->
- let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in
- tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
-
let gmake env sigma goal =
let state = get_state goal in
let goal = drop_state goal in
@@ -1258,9 +1251,9 @@ module V82 = struct
let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
{ Evd.it = goals ; sigma=solution; }
- let top_evars initial =
+ let top_evars initial { solution=sigma; } =
let evars_of_initial (c,_) =
- Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c))
+ Evar.Set.elements (Evd.evars_of_term sigma c)
in
CList.flatten (CList.map evars_of_initial initial)
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 9455dae643..b7ff3ac432 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -505,10 +505,6 @@ module Goal : sig
(** Type of goals. *)
type t
- (** Normalises the argument goal. *)
- val normalize : t -> t tactic
- [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"]
-
(** [concl], [hyps], [env] and [sigma] given a goal [gl] return
respectively the conclusion of [gl], the hypotheses of [gl], the
environment of [gl] (i.e. the global environment and the
@@ -599,7 +595,7 @@ module V82 : sig
val top_goals : entry -> proofview -> Evar.t list Evd.sigma
(* returns the existential variable used to start the proof *)
- val top_evars : entry -> Evar.t list
+ val top_evars : entry -> proofview -> Evar.t list
(* Caution: this function loses quite a bit of information. It
should be avoided as much as possible. It should work as
diff --git a/engine/termops.ml b/engine/termops.ml
index 8e12c9be88..fcacb53ac4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -25,11 +25,6 @@ module CompactedDecl = Context.Compacted.Declaration
module Internal = struct
-let pr_sort_family = Sorts.pr_sort_family
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-let pr_fix = Constr.debug_print_fix
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c)
let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c)
let term_printer = ref debug_print_constr_env
@@ -192,7 +187,7 @@ let compute_evar_dependency_graph sigma =
in
match evar_body evi with
| Evar_empty -> acc
- | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc
+ | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term sigma c) acc
in
Evd.fold fold sigma EvMap.empty
@@ -761,13 +756,6 @@ let fold_constr_with_binders sigma g f n acc c =
let c = Unsafe.to_constr (whd_evar sigma c) in
Constr.fold_constr_with_binders g f n acc c
-(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
- subterms of [c]; it carries an extra data [acc] which is processed by [g] at
- each binder traversal; it is not recursive and the order with which
- subterms are processed is not specified *)
-
-let iter_constr_with_full_binders = EConstr.iter_with_full_binders
-
(***************************)
(* occurs check functions *)
(***************************)
@@ -862,8 +850,6 @@ let collect_vars sigma c =
| _ -> EConstr.fold sigma aux vars c in
aux Id.Set.empty c
-let vars_of_global_reference = vars_of_global
-
(* Tests whether [m] is a subterm of [t]:
[m] is appropriately lifted through abstractions of [t] *)
@@ -1417,10 +1403,6 @@ let prod_applist_assum sigma n c l =
| _ -> anomaly (Pp.str "Not enough prod/let's.") in
app n [] c l
-let on_judgment = Environ.on_judgment
-let on_judgment_value = Environ.on_judgment_value
-let on_judgment_type = Environ.on_judgment_type
-
(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
variables skips let-in's; let-in's in the middle are put in ctx2 *)
let context_chop k ctx =
diff --git a/engine/termops.mli b/engine/termops.mli
index 1dd9941c5e..a9217b3586 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -16,12 +16,6 @@ open Constr
open Environ
open EConstr
-(** printers *)
-val pr_sort_family : Sorts.family -> Pp.t
-[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"]
-val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
-[@@ocaml.deprecated "Use [Constr.debug_print_fix]"]
-
(** about contexts *)
val push_rel_assum : Name.t Context.binder_annot * types -> env -> env
val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env
@@ -84,12 +78,6 @@ val fold_constr_with_full_binders : Evd.evar_map ->
('a -> 'b -> constr -> 'b) ->
'a -> 'b -> constr -> 'b
-val iter_constr_with_full_binders : Evd.evar_map ->
- (rel_declaration -> 'a -> 'a) ->
- ('a -> constr -> unit) -> 'a ->
- constr -> unit
-[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."]
-
(**********************************************************************)
val strip_head_cast : Evd.evar_map -> constr -> constr
@@ -121,9 +109,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int
val collect_metas : Evd.evar_map -> constr -> int list
val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
-val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
-[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
-
(* Substitution of metavariables *)
type meta_value_map = (metavariable * Constr.constr) list
val subst_meta : meta_value_map -> Constr.constr -> Constr.constr
@@ -292,15 +277,6 @@ val is_Type : Evd.evar_map -> constr -> bool
val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
-(** Combinators on judgments *)
-
-val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment]."]
-val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
-val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
-[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
-
(** {5 Debug pretty-printers} *)
open Evd
diff --git a/engine/uState.ml b/engine/uState.ml
index 6f4f40e2c5..adea78d4c9 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -85,7 +85,7 @@ let union ctx ctx' =
let declarenew g =
LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
in
- let names_rev = LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+ let names_rev = LMap.lunion (snd ctx.uctx_names) (snd ctx'.uctx_names) in
{ uctx_names = (names, names_rev);
uctx_local = local;
uctx_seff_univs = seff;
@@ -116,8 +116,6 @@ let univ_entry ~poly uctx =
Polymorphic_entry (nas, uctx)
else Monomorphic_entry (context_set uctx)
-let const_univ_entry = univ_entry
-
let of_context_set ctx = { empty with uctx_local = ctx }
let subst ctx = ctx.uctx_univ_variables
diff --git a/engine/uState.mli b/engine/uState.mli
index a358813825..3df7f9e8e9 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -67,9 +67,6 @@ val context : t -> Univ.UContext.t
val univ_entry : poly:bool -> t -> Entries.universes_entry
(** Pick from {!context} or {!context_set} based on [poly]. *)
-val const_univ_entry : poly:bool -> t -> Entries.universes_entry
-[@@ocaml.deprecated "Use [univ_entry]."]
-
(** {5 Constraints handling} *)
val drop_weak_constraints : bool ref
diff --git a/engine/univGen.ml b/engine/univGen.ml
index c310331b15..f1deb1bfaf 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -25,11 +25,6 @@ let new_univ_global () =
let fresh_level () =
Univ.Level.make (new_univ_global ())
-(* TODO: remove *)
-let new_univ () = Univ.Universe.make (fresh_level ())
-let new_Type () = mkType (new_univ ())
-let new_Type_sort () = sort_of_univ (new_univ ())
-
let fresh_instance auctx =
let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
let ctx = Array.fold_right LSet.add inst LSet.empty in
@@ -83,10 +78,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 constr_of_global gr = constr_of_monomorphic_global gr
-
-let constr_of_global_univ = mkRef
-
let fresh_global_or_constr_instance env = function
| IsConstr c -> c, ContextSet.empty
| IsGlobal gr -> fresh_global_instance env gr
@@ -99,34 +90,6 @@ let global_of_constr c =
| Var id -> VarRef id, Instance.empty
| _ -> raise Not_found
-open Declarations
-
-let type_of_reference env r =
- match r with
- | VarRef id -> Environ.named_type id env, ContextSet.empty
-
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- let ty = cb.const_type in
- let auctx = Declareops.constant_polymorphic_context cb in
- let inst, ctx = fresh_instance auctx in
- Vars.subst_instance_constr inst ty, ctx
-
- | IndRef ind ->
- let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
- let auctx = Declareops.inductive_polymorphic_context mib in
- let inst, ctx = fresh_instance auctx in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
-
- | ConstructRef (ind,_ as cstr) ->
- let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- let auctx = Declareops.inductive_polymorphic_context mib in
- let inst, ctx = fresh_instance auctx in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
-
-let type_of_global t = type_of_reference (Global.env ()) t
-
let fresh_sort_in_family = function
| InSProp -> Sorts.sprop, ContextSet.empty
| InProp -> Sorts.prop, ContextSet.empty
@@ -135,11 +98,6 @@ let fresh_sort_in_family = function
let u = fresh_level () in
sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
-let new_sort_in_family sf =
- fst (fresh_sort_in_family sf)
-
-let extend_context = Univ.extend_in_context_set
-
let new_global_univ () =
let u = fresh_level () in
(Univ.Universe.make u, ContextSet.singleton u)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index b4598e10d0..34920e5620 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -24,16 +24,7 @@ val new_univ_id : unit -> univ_unique_id (** for the stm *)
val new_univ_global : unit -> Level.UGlobal.t
val fresh_level : unit -> Level.t
-val new_univ : unit -> Universe.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type : unit -> types
-[@@ocaml.deprecated "Use [new_univ_level]"]
-val new_Type_sort : unit -> Sorts.t
-[@@ocaml.deprecated "Use [new_univ_level]"]
-
val new_global_univ : unit -> Universe.t in_universe_context_set
-val new_sort_in_family : Sorts.family -> Sorts.t
-[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
(** Build a fresh instance for a given context, its associated substitution and
the instantiated constraints. *)
@@ -66,27 +57,9 @@ val fresh_universe_context_set_instance : ContextSet.t ->
(** Raises [Not_found] if not a global reference. *)
val global_of_constr : constr -> GlobRef.t puniverses
-val constr_of_global_univ : GlobRef.t puniverses -> constr
-[@@ocaml.deprecated "Use [Constr.mkRef]"]
-
-val extend_context : 'a in_universe_context_set -> ContextSet.t ->
- 'a in_universe_context_set
-[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
-
(** Create a fresh global in the global environment, without side effects.
BEWARE: this raises an error on polymorphic constants/inductives:
the constraints should be properly added to an evd.
See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
the proper way to get a fresh copy of a polymorphic global reference. *)
val constr_of_monomorphic_global : GlobRef.t -> constr
-
-val constr_of_global : GlobRef.t -> constr
-[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\
- use [constr_of_monomorphic_global] if the reference is guaranteed to\
- be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"]
-
-(** Returns the type of the global reference, by creating a fresh instance of polymorphic
- references and computing their instantiated universe context. (side-effect on the
- universe counter, use with care). *)
-val type_of_global : GlobRef.t -> types in_universe_context_set
-[@@ocaml.deprecated "use [Typeops.type_of_global]"]
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 46ff6340b4..fcbf305f9d 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -203,7 +203,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
(acc, [], LMap.empty, LMap.empty) l
in
let left = CList.uniquize (List.filter (not_lower lower) left) in
- (acc, left, LMap.union newlow lower)
+ (acc, left, LMap.lunion newlow lower)
in
let instantiate_lbound lbound =
let alg = LSet.mem u algs in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:42:38 +0000