aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml3
-rw-r--r--engine/evarutil.mli6
-rw-r--r--engine/evd.ml24
-rw-r--r--engine/evd.mli53
-rw-r--r--engine/namegen.ml1
-rw-r--r--engine/nameops.ml26
-rw-r--r--engine/nameops.mli44
-rw-r--r--engine/proofview.ml7
-rw-r--r--engine/proofview.mli9
-rw-r--r--engine/termops.ml10
-rw-r--r--engine/termops.mli3
-rw-r--r--engine/uState.ml19
-rw-r--r--engine/uState.mli12
-rw-r--r--engine/univops.ml85
-rw-r--r--engine/univops.mli5
15 files changed, 45 insertions, 262 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index afedfe180b..648f960354 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -875,6 +875,3 @@ let eq_constr_univs_test sigma1 sigma2 t u =
(universes sigma2) fold t u sigma2
in
match ans with None -> false | Some _ -> true
-
-type type_constraint = EConstr.types option
-type val_constraint = EConstr.constr option
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 3ab2d3e348..f271c14ea2 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -259,12 +259,6 @@ val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Lo
val meta_counter_summary_tag : int Summary.Dyn.tag
-(** Deprecated *)
-type type_constraint = types option
-[@@ocaml.deprecated "use the version in Evardefine"]
-type val_constraint = constr option
-[@@ocaml.deprecated "use the version in Evardefine"]
-
val e_new_evar :
env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
diff --git a/engine/evd.ml b/engine/evd.ml
index 78d5d4c8ff..0c9c3a29b2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -132,8 +132,6 @@ end
module Store = Store.Make ()
-type evar = Evar.t
-
let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
type evar_body =
@@ -1206,28 +1204,6 @@ module Monad =
type unsolvability_explanation = SeveralInstancesFound of int
-(** Deprecated *)
-type evar_universe_context = UState.t
-let empty_evar_universe_context = UState.empty
-let union_evar_universe_context = UState.union
-let evar_universe_context_set = UState.context_set
-let evar_universe_context_constraints = UState.constraints
-let evar_context_universe_context = UState.context
-let evar_universe_context_of = UState.of_context_set
-let evar_universe_context_subst = UState.subst
-let add_constraints_context = UState.add_constraints
-let constrain_variables = UState.constrain_variables
-let evar_universe_context_of_binders = UState.of_binders
-let make_evar_universe_context e l =
- let g = Environ.universes e in
- match l with
- | None -> UState.make g
- | Some l -> UState.make_with_initial_binders g l
-let normalize_evar_universe_context_variables = UState.normalize_variables
-let abstract_undefined_variables = UState.abstract_undefined_variables
-let normalize_evar_universe_context = UState.minimize
-let nf_constraints = minimize_universes
-
module MiniEConstr = struct
module ESorts =
diff --git a/engine/evd.mli b/engine/evd.mli
index b2670ee518..c40e925d81 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -33,14 +33,6 @@ type etypes = econstr
(** {5 Existential variables and unification states} *)
-type evar = Evar.t
-[@@ocaml.deprecated "use Evar.t"]
-(** Existential variables. *)
-
-(** {6 Evars} *)
-val string_of_existential : Evar.t -> string
-[@@ocaml.deprecated "use Evar.print"]
-
(** {6 Evar filters} *)
module Filter :
@@ -130,10 +122,6 @@ val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
(** {6 Unification state} **)
-type evar_universe_context = UState.t
-[@@ocaml.deprecated "Alias of UState.t"]
-(** The universe context associated to an evar map *)
-
type evar_map
(** Type of unification state. Essentially a bunch of state-passing data needed
to handle incremental term construction. *)
@@ -529,48 +517,11 @@ val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * UState.t
-val evar_universe_context_set : UState.t -> Univ.ContextSet.t
-[@@ocaml.deprecated "Alias of UState.context_set"]
-val evar_universe_context_constraints : UState.t -> Univ.Constraint.t
-[@@ocaml.deprecated "Alias of UState.constraints"]
-val evar_context_universe_context : UState.t -> Univ.UContext.t
-[@@ocaml.deprecated "alias of UState.context"]
-
-val evar_universe_context_of : Univ.ContextSet.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.of_context_set"]
-val empty_evar_universe_context : UState.t
-[@@ocaml.deprecated "Alias of UState.empty"]
-val union_evar_universe_context : UState.t -> UState.t ->
- UState.t
-[@@ocaml.deprecated "Alias of UState.union"]
-val evar_universe_context_subst : UState.t -> UnivSubst.universe_opt_subst
-[@@ocaml.deprecated "Alias of UState.subst"]
-val constrain_variables : Univ.LSet.t -> UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.constrain_variables"]
-
-
-val evar_universe_context_of_binders :
- UnivNames.universe_binders -> UState.t
-[@@ocaml.deprecated "Alias of UState.of_binders"]
-
-val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t
-[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"]
val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map
(** Raises Not_found if not a name for a universe in this map. *)
val universe_of_name : evar_map -> Id.t -> Univ.Level.t
val universe_binders : evar_map -> UnivNames.universe_binders
-val add_constraints_context : UState.t ->
- Univ.Constraint.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.add_constraints"]
-
-
-val normalize_evar_universe_context_variables : UState.t ->
- Univ.universe_subst in_evar_universe_context
-[@@ocaml.deprecated "Alias of UState.normalize_variables"]
-
-val normalize_evar_universe_context : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.minimize"]
val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
@@ -627,8 +578,6 @@ val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map
val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
-val abstract_undefined_variables : UState.t -> UState.t
-[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"]
val fix_undefined_variables : evar_map -> evar_map
@@ -636,8 +585,6 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
(** Universe minimization *)
val minimize_universes : evar_map -> evar_map
-val nf_constraints : evar_map -> evar_map
-[@@ocaml.deprecated "Alias of Evd.minimize_universes"]
val update_sigma_env : evar_map -> env -> evar_map
diff --git a/engine/namegen.ml b/engine/namegen.ml
index d66b77b573..c069ec5a06 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -17,6 +17,7 @@
open Util
open Names
open Term
+open Constr
open Environ
open EConstr
open Vars
diff --git a/engine/nameops.ml b/engine/nameops.ml
index 53969cafa8..735a59fe51 100644
--- a/engine/nameops.ml
+++ b/engine/nameops.ml
@@ -11,10 +11,6 @@
open Util
open Names
-(* Identifiers *)
-
-let pr_id id = Id.print id
-
(* Utilities *)
let code_of_0 = Char.code '0'
@@ -191,28 +187,6 @@ struct
end
-open Name
-
-(* Compatibility *)
-let out_name = get_id
-let name_fold = fold_right
-let name_iter = iter
-let name_app = map
-let name_fold_map = fold_left_map
-let name_cons = cons
-let name_max = pick
-let pr_name = print
-
-let pr_lab l = Label.print l
-
(* Metavariables *)
let pr_meta = Pp.int
let string_of_meta = string_of_int
-
-(* Deprecated *)
-open Libnames
-let default_library = default_library
-let coq_string = coq_string
-let coq_root = coq_root
-let default_root_prefix = default_root_prefix
-
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 96842dfb99..8a93fad8cc 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -94,47 +94,3 @@ end
(** Metavariables *)
val pr_meta : Constr.metavariable -> Pp.t
val string_of_meta : Constr.metavariable -> string
-
-val out_name : Name.t -> Id.t
-[@@ocaml.deprecated "Same as [Name.get_id]"]
-
-val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
-[@@ocaml.deprecated "Same as [Name.fold_right]"]
-
-val name_iter : (Id.t -> unit) -> Name.t -> unit
-[@@ocaml.deprecated "Same as [Name.iter]"]
-
-val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.map]"]
-
-val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-[@@ocaml.deprecated "Same as [Name.fold_left_map]"]
-
-val name_max : Name.t -> Name.t -> Name.t
-[@@ocaml.deprecated "Same as [Name.pick]"]
-
-val name_cons : Name.t -> Id.t list -> Id.t list
-[@@ocaml.deprecated "Same as [Name.cons]"]
-
-val pr_name : Name.t -> Pp.t
-[@@ocaml.deprecated "Same as [Name.print]"]
-
-val pr_id : Id.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Id.print]"]
-
-val pr_lab : Label.t -> Pp.t
-[@@ocaml.deprecated "Same as [Names.Label.print]"]
-
-(** Deprecated stuff to libnames *)
-val default_library : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_library]"]
-
-val coq_root : module_ident (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_root]"]
-
-val coq_string : string (** "Coq" *)
-[@@ocaml.deprecated "Same as [Libnames.coq_string]"]
-
-val default_root_prefix : DirPath.t
-[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"]
-
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 54237ceb41..fdb0a215d3 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1085,8 +1085,6 @@ module Goal = struct
self : Evar.t ; (* for compatibility with old-style definitions *)
}
- let assume (gl : t) = (gl : t)
-
let print { sigma; self } = { Evd.it = self; sigma }
let state { state=state } = state
@@ -1274,11 +1272,6 @@ module V82 = struct
- (* Returns the open goals of the proofview together with the evar_map to
- interpret them. *)
- let goals { comb = comb ; solution = solution; } =
- { Evd.it = List.map drop_state comb ; sigma = solution }
-
let top_goals initial { solution=solution; } =
let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
{ Evd.it = goals ; sigma=solution; }
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 1905686fe7..970bf67732 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -495,10 +495,6 @@ module Goal : sig
(** Type of goals. *)
type t
- (** Assume that you do not need the goal to be normalized. *)
- val assume : t -> t
- [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"]
-
(** Normalises the argument goal. *)
val normalize : t -> t tactic
@@ -589,11 +585,6 @@ module V82 : sig
(in chronological order of insertion). *)
val grab : proofview -> proofview
- (* Returns the open goals of the proofview together with the evar_map to
- interpret them. *)
- val goals : proofview -> Evar.t list Evd.sigma
- [@@ocaml.deprecated "Use [Proofview.proofview]"]
-
val top_goals : entry -> proofview -> Evar.t list Evd.sigma
(* returns the existential variable used to start the proof *)
diff --git a/engine/termops.ml b/engine/termops.ml
index c52f960799..0c567754ad 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -857,6 +857,13 @@ let occur_meta_or_existential sigma c =
| _ -> EConstr.iter sigma occrec c
in try occrec c; false with Occur -> true
+let occur_metavariable sigma m c =
+ let rec occrec c = match EConstr.kind sigma c with
+ | Meta m' -> if Int.equal m m' then raise Occur
+ | _ -> EConstr.iter sigma occrec c
+ in
+ try occrec c; false with Occur -> true
+
let occur_evar sigma n c =
let rec occur_rec c = match EConstr.kind sigma c with
| Evar (sp,_) when Evar.equal sp n -> raise Occur
@@ -974,9 +981,6 @@ let count_occurrences sigma m t =
countrec m t;
!n
-(* Synonymous *)
-let occur_term = dependent
-
let pop t = EConstr.Vars.lift (-1) t
(***************************)
diff --git a/engine/termops.mli b/engine/termops.mli
index e2ddcd36e7..6e63539ca3 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -94,6 +94,7 @@ exception Occur
val occur_meta : Evd.evar_map -> constr -> bool
val occur_existential : Evd.evar_map -> constr -> bool
val occur_meta_or_existential : Evd.evar_map -> constr -> bool
+val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
val occur_var_in_decl :
@@ -113,8 +114,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
-val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *)
-[@@ocaml.deprecated "alias of Termops.dependent"]
(* Substitution of metavariables *)
type meta_value_map = (metavariable * Constr.constr) list
diff --git a/engine/uState.ml b/engine/uState.ml
index 844eb390b7..643c621fd5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -305,8 +305,20 @@ let reference_of_level uctx =
let pr_uctx_level uctx l =
Libnames.pr_reference (reference_of_level uctx l)
+type ('a, 'b) gen_universe_decl = {
+ univdecl_instance : 'a; (* Declared universes *)
+ univdecl_extensible_instance : bool; (* Can new universes be added *)
+ univdecl_constraints : 'b; (* Declared constraints *)
+ univdecl_extensible_constraints : bool (* Can new constraints be added *) }
+
type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+
+let default_univ_decl =
+ { univdecl_instance = [];
+ univdecl_extensible_instance = true;
+ univdecl_constraints = Univ.Constraint.empty;
+ univdecl_extensible_constraints = true }
let error_unbound_universes left uctx =
let open Univ in
@@ -367,7 +379,6 @@ let check_implication uctx cstrs cstrs' =
(str "Universe constraints are not implied by the ones declared.")
let check_mono_univ_decl uctx decl =
- let open Misctypes in
let () =
let names = decl.univdecl_instance in
let extensible = decl.univdecl_extensible_instance in
@@ -380,7 +391,6 @@ let check_mono_univ_decl uctx decl =
uctx.uctx_local
let check_univ_decl ~poly uctx decl =
- let open Misctypes in
let ctx =
let names = decl.univdecl_instance in
let extensible = decl.univdecl_extensible_instance in
@@ -663,6 +673,3 @@ let update_sigma_env uctx env =
let pr_weak prl {uctx_weak_constraints=weak} =
let open Pp in
prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
-
-(** Deprecated *)
-let normalize = minimize
diff --git a/engine/uState.mli b/engine/uState.mli
index 11aaaf3892..e2f25642e5 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -137,11 +137,17 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
(** Universe minimization *)
val minimize : t -> t
-val normalize : t -> t
-[@@ocaml.deprecated "Alias of UState.minimize"]
+
+type ('a, 'b) gen_universe_decl = {
+ univdecl_instance : 'a; (* Declared universes *)
+ univdecl_extensible_instance : bool; (* Can new universes be added *)
+ univdecl_constraints : 'b; (* Declared constraints *)
+ univdecl_extensible_constraints : bool (* Can new constraints be added *) }
type universe_decl =
- (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+ (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+
+val default_univ_decl : universe_decl
(** [check_univ_decl ctx decl]
diff --git a/engine/univops.ml b/engine/univops.ml
index 76dbaa250a..3fd518490a 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -35,79 +35,14 @@ let universes_of_constr env c =
| _ -> Constr.fold aux s c
in aux LSet.empty c
-type graphnode = {
- mutable up : constraint_type LMap.t;
- mutable visited : bool
-}
-
-let merge_types d d0 =
- match d, d0 with
- | _, Lt | Lt, _ -> Lt
- | Le, _ | _, Le -> Le
- | Eq, Eq -> Eq
-
-let merge_up d b up =
- let find = try Some (LMap.find b up) with Not_found -> None in
- match find with
- | Some d0 ->
- let d = merge_types d d0 in
- if d == d0 then up else LMap.add b d up
- | None -> LMap.add b d up
-
-let add_up a d b graph =
- let node, graph =
- try LMap.find a graph, graph
- with Not_found ->
- let node = { up = LMap.empty; visited = false } in
- node, LMap.add a node graph
- in
- node.up <- merge_up d b node.up;
- graph
-
-(* for each node transitive close until you find a non removable, discard the rest *)
-let transitive_close removable graph =
- let rec do_node a node =
- if not node.visited
- then
- let keepup =
- LMap.fold (fun b d keepup ->
- if not (LSet.mem b removable)
- then merge_up d b keepup
- else
- begin
- match LMap.find b graph with
- | bnode ->
- do_node b bnode;
- LMap.fold (fun k d' keepup ->
- merge_up (merge_types d d') k keepup)
- bnode.up keepup
- | exception Not_found -> keepup
- end
- )
- node.up LMap.empty
- in
- node.up <- keepup;
- node.visited <- true
- in
- LMap.iter do_node graph
-
-let restrict_universe_context (univs,csts) keep =
- let removable = LSet.diff univs keep in
- let (csts, rem) =
- Constraint.fold (fun (a,d,b as cst) (csts, rem) ->
- if LSet.mem a removable || LSet.mem b removable
- then (csts, add_up a d b rem)
- else (Constraint.add cst csts, rem))
- csts (Constraint.empty, LMap.empty)
- in
- transitive_close removable rem;
- let csts =
- LMap.fold (fun a node csts ->
- if LSet.mem a removable
- then csts
- else
- LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts)
- node.up csts)
- rem csts
- in
+let restrict_universe_context (univs, csts) keep =
+ let removed = LSet.diff univs keep in
+ if LSet.is_empty removed then univs, csts
+ else
+ let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+ let g = UGraph.empty_universes in
+ let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+ let g = UGraph.merge_constraints csts g in
+ let allkept = LSet.diff allunivs removed in
+ let csts = UGraph.constraints_for ~kept:allkept g in
(LSet.inter univs keep, csts)
diff --git a/engine/univops.mli b/engine/univops.mli
index d1585414c1..0b37ab975d 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -14,5 +14,8 @@ open Univ
(** The universes of monomorphic constants appear. *)
val universes_of_constr : Environ.env -> constr -> LSet.t
-(** Shrink a universe context to a restricted set of variables *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+ the universes in [keep]. The constraints [csts] are adjusted so
+ that transitive constraints between remaining universes (those in
+ [keep] and those not in [univs]) are preserved. *)
val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:24:14 +0000