aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml11
-rw-r--r--engine/eConstr.mli8
-rw-r--r--engine/evarutil.ml17
-rw-r--r--engine/evarutil.mli8
-rw-r--r--engine/evd.ml42
-rw-r--r--engine/evd.mli58
-rw-r--r--engine/geninterp.ml6
-rw-r--r--engine/geninterp.mli4
-rw-r--r--engine/namegen.ml27
-rw-r--r--engine/namegen.mli10
-rw-r--r--engine/termops.ml55
-rw-r--r--engine/termops.mli8
-rw-r--r--engine/uState.ml4
-rw-r--r--engine/uState.mli14
-rw-r--r--engine/universes.ml27
-rw-r--r--engine/universes.mli80
16 files changed, 200 insertions, 179 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index a54c082979..bcfbc8081e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -10,6 +10,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Context
open Evd
@@ -34,7 +35,7 @@ end
type t
val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
-val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
+val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
val whd_evar : Evd.evar_map -> t -> t
val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
val of_constr : Constr.t -> t
@@ -84,16 +85,16 @@ let rec whd_evar sigma c =
| Some c -> whd_evar sigma c
| None -> c
end
- | App (f, args) when isEvar f ->
+ | App (f, args) when Term.isEvar f ->
(** Enforce smart constructor invariant on applications *)
- let ev = destEvar f in
+ let ev = Term.destEvar f in
begin match safe_evar_value sigma ev with
| None -> c
| Some f -> whd_evar sigma (mkApp (f, args))
end
- | Cast (c0, k, t) when isEvar c0 ->
+ | Cast (c0, k, t) when Term.isEvar c0 ->
(** Enforce smart constructor invariant on casts. *)
- let ev = destEvar c0 in
+ let ev = Term.destEvar c0 in
begin match safe_evar_value sigma ev with
| None -> c
| Some c -> whd_evar sigma (mkCast (c, k, t))
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 4dbf6c18a3..e9ef302cf6 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -93,14 +93,14 @@ val mkEvar : t pexistential -> t
val mkSort : Sorts.t -> t
val mkProp : t
val mkSet : t
-val mkType : Univ.universe -> t
+val mkType : Univ.Universe.t -> t
val mkCast : t * cast_kind * t -> t
val mkProd : Name.t * t * t -> t
val mkLambda : Name.t * t * t -> t
val mkLetIn : Name.t * t * t * t -> t
val mkApp : t * t array -> t
-val mkConst : constant -> t
-val mkConstU : constant * EInstance.t -> t
+val mkConst : Constant.t -> t
+val mkConstU : Constant.t * EInstance.t -> t
val mkProj : (projection * t) -> t
val mkInd : inductive -> t
val mkIndU : inductive * EInstance.t -> t
@@ -157,7 +157,7 @@ val destProd : Evd.evar_map -> t -> Name.t * types * types
val destLambda : Evd.evar_map -> t -> Name.t * types * t
val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
val destApp : Evd.evar_map -> t -> t * t array
-val destConst : Evd.evar_map -> t -> constant * EInstance.t
+val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
val destEvar : Evd.evar_map -> t -> t pexistential
val destInd : Evd.evar_map -> t -> inductive * EInstance.t
val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index eabfb7b398..df4ef2ce71 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -10,6 +10,7 @@ open CErrors
open Util
open Names
open Term
+open Constr
open Termops
open Namegen
open Pre_env
@@ -56,12 +57,12 @@ let new_global evd x =
exception Uninstantiated_evar of existential_key
let rec flush_and_check_evars sigma c =
- match kind_of_term c with
+ match kind c with
| Evar (evk,_ as ev) ->
(match existential_opt_value sigma ev with
| None -> raise (Uninstantiated_evar evk)
| Some c -> flush_and_check_evars sigma c)
- | _ -> map_constr (flush_and_check_evars sigma) c
+ | _ -> Constr.map (flush_and_check_evars sigma) c
let flush_and_check_evars sigma c =
flush_and_check_evars sigma (EConstr.Unsafe.to_constr c)
@@ -162,7 +163,7 @@ exception NoHeadEvar
let head_evar sigma c =
(** FIXME: this breaks if using evar-insensitive code *)
let c = EConstr.Unsafe.to_constr c in
- let rec hrec c = match kind_of_term c with
+ let rec hrec c = match kind c with
| Evar (evk,_) -> evk
| Case (_,_,c,_) -> hrec c
| App (c,_) -> hrec c
@@ -306,7 +307,7 @@ let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
in
let extract_if_neq id = function
| Anonymous -> None
- | Name id' when id_ord id id' = 0 -> None
+ | Name id' when Id.compare id id' = 0 -> None
| Name id' -> Some id'
in
let na = RelDecl.get_name decl in
@@ -485,7 +486,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
(ie the hypotheses ids have been removed from the contexts of
evars). [global] should be true iff there is some variable of [ids] which
is a section variable *)
- match kind_of_term c with
+ match kind c with
| Var id' ->
if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
@@ -552,7 +553,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
evdref := evd;
Evd.existential_value !evdref ev
- | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
+ | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c
let clear_hyps_in_evi_main env evdref hyps terms ids =
(* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
@@ -696,10 +697,10 @@ let undefined_evars_of_evar_info evd evi =
do not have this luxury, and need the more complete version. *)
let occur_evar_upto sigma n c =
let c = EConstr.Unsafe.to_constr c in
- let rec occur_rec c = match kind_of_term c with
+ let rec occur_rec c = match kind c with
| Evar (sp,_) when Evar.equal sp n -> raise Occur
| Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
- | _ -> iter_constr occur_rec c
+ | _ -> Constr.iter occur_rec c
in
try occur_rec c; false with Occur -> true
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ee0fae3d46..62288ced46 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Evd
open Environ
open EConstr
@@ -54,11 +54,11 @@ val e_new_evar :
val new_type_evar :
env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
- evar_map * (constr * sorts)
+ evar_map * (constr * Sorts.t)
val e_new_type_evar : env -> evar_map ref ->
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
+ ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t
val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
@@ -223,7 +223,7 @@ val push_rel_decl_to_named_context :
evar_map -> rel_declaration -> ext_named_context -> ext_named_context
val push_rel_context_to_named_context : Environ.env -> evar_map -> types ->
- named_context_val * types * constr list * csubst * (identifier*constr) list
+ named_context_val * types * constr list * csubst * (Id.t*constr) list
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
diff --git a/engine/evd.ml b/engine/evd.ml
index 324f883e8e..a1cb0ec68e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -8,10 +8,11 @@
open Pp
open CErrors
+open Sorts
open Util
open Names
open Nameops
-open Term
+open Constr
open Vars
open Environ
@@ -124,10 +125,9 @@ end
(* The type of mappings for existential variables *)
-module Dummy = struct end
-module Store = Store.Make(Dummy)
+module Store = Store.Make ()
-type evar = Term.existential_key
+type evar = existential_key
let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk)
@@ -243,7 +243,7 @@ let evar_instance_array test_id info args =
instrec filter (evar_context info) 0
let make_evar_instance_array info args =
- evar_instance_array (NamedDecl.get_id %> isVarId) info args
+ evar_instance_array (NamedDecl.get_id %> Term.isVarId) info args
let instantiate_evar_array info c args =
let inst = make_evar_instance_array info args in
@@ -281,9 +281,9 @@ type 'a freelisted = {
(* Collects all metavars appearing in a constr *)
let metavars_of c =
let rec collrec acc c =
- match kind_of_term c with
+ match kind c with
| Meta mv -> Int.Set.add mv acc
- | _ -> Term.fold_constr collrec acc c
+ | _ -> Constr.fold collrec acc c
in
collrec Int.Set.empty c
@@ -371,17 +371,17 @@ val key : Id.t -> t -> Evar.t
end =
struct
-type t = Id.t EvMap.t * existential_key Idmap.t
+type t = Id.t EvMap.t * existential_key Id.Map.t
-let empty = (EvMap.empty, Idmap.empty)
+let empty = (EvMap.empty, Id.Map.empty)
let add_name_newly_undefined id evk evi (evtoid, idtoev as names) =
match id with
| None -> names
| Some id ->
- if Idmap.mem id idtoev then
+ if Id.Map.mem id idtoev then
user_err (str "Already an existential evar of name " ++ pr_id id);
- (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+ (EvMap.add evk id evtoid, Id.Map.add id evk idtoev)
let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
if EvMap.mem evk evtoid then
@@ -393,15 +393,15 @@ let remove_name_defined evk (evtoid, idtoev as names) =
let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
match id with
| None -> names
- | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+ | Some id -> (EvMap.remove evk evtoid, Id.Map.remove id idtoev)
let rename evk id (evtoid, idtoev) =
let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in
match id' with
- | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+ | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev)
| Some id' ->
- if Idmap.mem id idtoev then anomaly (str "Evar name already in use.");
- (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
+ if Id.Map.mem id idtoev then anomaly (str "Evar name already in use.");
+ (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev))
let reassign_name_defined evk evk' (evtoid, idtoev as names) =
let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
@@ -409,13 +409,13 @@ let reassign_name_defined evk evk' (evtoid, idtoev as names) =
| None -> names (** evk' must not be defined *)
| Some id ->
(EvMap.add evk' id (EvMap.remove evk evtoid),
- Idmap.add id evk' (Idmap.remove id idtoev))
+ Id.Map.add id evk' (Id.Map.remove id idtoev))
let ident evk (evtoid, _) =
try Some (EvMap.find evk evtoid) with Not_found -> None
let key id (_, idtoev) =
- Idmap.find id idtoev
+ Id.Map.find id idtoev
end
@@ -707,10 +707,10 @@ let extract_all_conv_pbs evd =
extract_conv_pbs evd (fun _ -> true)
let loc_of_conv_pb evd (pbty,env,t1,t2) =
- match kind_of_term (fst (decompose_app t1)) with
+ match kind (fst (Term.decompose_app t1)) with
| Evar (evk1,_) -> fst (evar_source evk1 evd)
| _ ->
- match kind_of_term (fst (decompose_app t2)) with
+ match kind (fst (Term.decompose_app t2)) with
| Evar (evk2,_) -> fst (evar_source evk2 evd)
| _ -> None
@@ -721,9 +721,9 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) =
let evars_of_term c =
let rec evrec acc c =
- match kind_of_term c with
+ match kind c with
| Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l)
- | _ -> Term.fold_constr evrec acc c
+ | _ -> Constr.fold evrec acc c
in
evrec Evar.Set.empty c
diff --git a/engine/evd.mli b/engine/evd.mli
index 96e4b6acce..45ca1a365a 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -9,7 +9,7 @@
open Util
open Loc
open Names
-open Term
+open Constr
open Environ
(** This file defines the pervasive unification state used everywhere in Coq
@@ -488,10 +488,10 @@ val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * evar_universe_context
-val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_set : evar_universe_context -> Univ.ContextSet.t
val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
-val evar_context_universe_context : evar_universe_context -> Univ.universe_context
-val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
+val evar_context_universe_context : evar_universe_context -> Univ.UContext.t
+val evar_universe_context_of : Univ.ContextSet.t -> evar_universe_context
val empty_evar_universe_context : evar_universe_context
val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
evar_universe_context
@@ -503,10 +503,10 @@ val evar_universe_context_of_binders :
Universes.universe_binders -> evar_universe_context
val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
-val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map
+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 -> string -> Univ.universe_level
-val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map
+val universe_of_name : evar_map -> string -> Univ.Level.t
+val add_universe_name : evar_map -> string -> Univ.Level.t -> evar_map
val add_constraints_context : evar_universe_context ->
Univ.constraints -> evar_universe_context
@@ -518,50 +518,50 @@ val normalize_evar_universe_context_variables : evar_universe_context ->
val normalize_evar_universe_context : evar_universe_context ->
evar_universe_context
-val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level
-val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.universe
-val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts
+val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Univ.Universe.t
+val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * Sorts.t
val add_global_univ : evar_map -> Univ.Level.t -> evar_map
val universe_rigidity : evar_map -> Univ.Level.t -> rigid
-val make_flexible_variable : evar_map -> algebraic:bool -> Univ.universe_level -> evar_map
+val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map
(** See [UState.make_flexible_variable] *)
-val is_sort_variable : evar_map -> sorts -> Univ.universe_level option
+val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option
(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
not a local sort variable declared in [evm] *)
val is_flexible_level : evar_map -> Univ.Level.t -> bool
-(* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *)
-val normalize_universe : evar_map -> Univ.universe -> Univ.universe
-val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance
+(* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *)
+val normalize_universe : evar_map -> Univ.Universe.t -> Univ.Universe.t
+val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t
-val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map
-val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map
-val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map
-val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
-val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
+val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
+val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
+val has_lub : evar_map -> Univ.Universe.t -> Univ.Universe.t -> evar_map
+val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
+val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
val set_eq_instances : ?flex:bool ->
- evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map
+ evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map
-val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool
-val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool
+val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
+val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
val evar_universe_context : evar_map -> evar_universe_context
-val universe_context_set : evar_map -> Univ.universe_context_set
+val universe_context_set : evar_map -> Univ.ContextSet.t
val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
- (Id.t * Univ.Level.t) list * Univ.universe_context
+ (Id.t * Univ.Level.t) list * Univ.UContext.t
val universe_subst : evar_map -> Universes.universe_opt_subst
val universes : evar_map -> UGraph.t
val check_univ_decl : evar_map -> UState.universe_decl ->
- Universes.universe_binders * Univ.universe_context
+ Universes.universe_binders * Univ.UContext.t
val merge_universe_context : evar_map -> evar_universe_context -> evar_map
val set_universe_context : evar_map -> evar_universe_context -> evar_map
-val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map
+val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map
val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
@@ -579,8 +579,8 @@ val update_sigma_env : evar_map -> env -> evar_map
(** Polymorphic universes *)
-val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
-val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> 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
diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index e79e258fbc..768ef3cfd9 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -9,11 +9,11 @@
open Names
open Genarg
-module TacStore = Store.Make(struct end)
+module TacStore = Store.Make ()
(** Dynamic toplevel values *)
-module ValT = Dyn.Make(struct end)
+module ValT = Dyn.Make ()
module Val =
struct
@@ -47,6 +47,8 @@ struct
end
+module ValTMap = ValT.Map
+
module ValReprObj =
struct
type ('raw, 'glb, 'top) obj = 'top Val.tag
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 492e372adb..ae0b26e594 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -39,6 +39,10 @@ sig
val inject : 'a tag -> 'a -> t
end
+
+module ValTMap (M : Dyn.TParam) :
+ Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+
(** Dynamic types for toplevel values. While the generic types permit to relate
objects at various levels of interpretation, toplevel values are wearing
their own type regardless of where they came from. This allows to use the
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 2e62b89011..ff0b5a74e7 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -61,9 +61,9 @@ let is_imported_ref = function
| VarRef _ -> false
| IndRef (kn,_)
| ConstructRef ((kn,_),_) ->
- let (mp,_,_) = repr_mind kn in is_imported_modpath mp
+ let (mp,_,_) = MutInd.repr3 kn in is_imported_modpath mp
| ConstRef kn ->
- let (mp,_,_) = repr_con kn in is_imported_modpath mp
+ let (mp,_,_) = Constant.repr3 kn in is_imported_modpath mp
let is_global id =
try
@@ -99,7 +99,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
match EConstr.kind sigma c with
| Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c)
| Cast (c,_,_) | App (c,_) -> hdrec c
- | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn)))
+ | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn)))
| Const _ | Ind _ | Construct _ | Var _ as c ->
Some (basename_of_global (global_of_constr c))
| Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
@@ -130,10 +130,10 @@ let hdchar env sigma c =
match EConstr.kind sigma c with
| Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c
| Cast (c,_,_) | App (c,_) -> hdrec k c
- | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn)))
- | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn))
- | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x))
- | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x))
+ | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
+ | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
+ | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
+ | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
| Var id -> lowercase_first_char id
| Sort s -> sort_hdchar (ESorts.kind sigma s)
| Rel n ->
@@ -376,15 +376,22 @@ let next_name_for_display sigma flags =
| RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t
(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let compute_displayed_name_in sigma flags avoid na c =
+let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c =
match na with
- | Anonymous when noccurn sigma 1 c ->
+ | Anonymous when noccurn_fun sigma 1 c ->
(Anonymous,avoid)
| _ ->
let fresh_id = next_name_for_display sigma flags na avoid in
- let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
+ let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in
(idopt, Id.Set.add fresh_id avoid)
+let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn
+
+let compute_displayed_name_in_gen f sigma =
+ (* only flag which does not need a constr, maybe to be refined *)
+ let flag = RenamingForGoal in
+ compute_displayed_name_in_gen_poly f sigma flag
+
let compute_and_force_displayed_name_in sigma flags avoid na c =
match na with
| Anonymous when noccurn sigma 1 c ->
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 6fde90a39c..abeed9f62d 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -9,7 +9,6 @@
(** This file features facilities to generate fresh names. *)
open Names
-open Term
open Environ
open Evd
open EConstr
@@ -27,7 +26,7 @@ val default_dependent_ident : Id.t (* "x" *)
Generating "intuitive" names from their type *)
val lowercase_first_char : Id.t -> string
-val sort_hdchar : sorts -> string
+val sort_hdchar : Sorts.t -> string
val hdchar : env -> evar_map -> types -> string
val id_of_name_using_hdchar : env -> evar_map -> types -> Name.t -> Id.t
val named_hd : env -> evar_map -> types -> Name.t -> Name.t
@@ -106,10 +105,15 @@ val compute_displayed_name_in :
val compute_and_force_displayed_name_in :
evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
val compute_displayed_let_name_in :
- evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
+ evar_map -> renaming_flags -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
val rename_bound_vars_as_displayed :
evar_map -> Id.Set.t -> Name.t list -> types -> types
+(* Generic function expecting a "not occurn" function *)
+val compute_displayed_name_in_gen :
+ (evar_map -> int -> 'a -> bool) ->
+ evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
+
(**********************************************************************)
(* Naming strategy for arguments in Prop when eliminating inductive types *)
diff --git a/engine/termops.ml b/engine/termops.ml
index b7fa2dc4a4..78dbdb11aa 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -12,6 +12,7 @@ open Util
open Names
open Nameops
open Term
+open Constr
open Vars
open Environ
@@ -31,7 +32,7 @@ let pr_sort_family = function
| InProp -> (str "Prop")
| InType -> (str "Type")
-let pr_con sp = str(string_of_con sp)
+let pr_con sp = str(Constant.to_string sp)
let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
@@ -46,7 +47,7 @@ let pr_puniverses p u =
if Univ.Instance.is_empty u then p
else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
-let rec pr_constr c = match kind_of_term c with
+let rec pr_constr c = match kind c with
| Rel n -> str "#"++int n
| Meta n -> str "Meta(" ++ int n ++ str ")"
| Var id -> pr_id id
@@ -74,9 +75,9 @@ let rec pr_constr c = match kind_of_term c with
(str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
| Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")"
- | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")"
+ | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
| Construct (((sp,i),j),u) ->
- str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
+ str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
| Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
| Case (ci,p,c,bl) -> v 0
(hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
@@ -327,11 +328,11 @@ let pr_evar_constraints sigma pbs =
Namegen.make_all_name_different env sigma
in
print_env_short env ++ spc () ++ str "|-" ++ spc () ++
- print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++
+ protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++
str (match pbty with
| Reduction.CONV -> "=="
| Reduction.CUMUL -> "<=") ++
- spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2)
+ spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2)
in
prlist_with_sep fnl pr_evconstr pbs
@@ -358,37 +359,37 @@ let pr_evar_list sigma l =
h 0 (str (string_of_existential ev) ++
str "==" ++ pr_evar_info evi ++
(if evi.evar_body == Evar_empty
- then str " {" ++ pr_existential_key sigma ev ++ str "}"
+ then str " {" ++ pr_existential_key sigma ev ++ str "}"
else mt ()))
in
h 0 (prlist_with_sep fnl pr l)
-let pr_evar_by_depth depth sigma = match depth with
-| None ->
- (* Print all evars *)
- let to_list d =
- let open Evd in
- (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
- let l = ref [] in
- let fold_def evk evi () = match evi.evar_body with
+let to_list d =
+ let open Evd in
+ (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *)
+ let l = ref [] in
+ let fold_def evk evi () = match evi.evar_body with
| Evar_defined _ -> l := (evk, evi) :: !l
| Evar_empty -> ()
- in
- let fold_undef evk evi () = match evi.evar_body with
+ in
+ let fold_undef evk evi () = match evi.evar_body with
| Evar_empty -> l := (evk, evi) :: !l
| Evar_defined _ -> ()
- in
- Evd.fold fold_def d ();
- Evd.fold fold_undef d ();
- !l
in
- str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl()
-| Some n ->
+ Evd.fold fold_def d ();
+ Evd.fold fold_undef d ();
+ !l
+
+let pr_evar_by_depth depth sigma = match depth with
+| None ->
(* Print all evars *)
+ str"EVARS:" ++ brk(0,1) ++ pr_evar_list sigma (to_list sigma) ++ fnl()
+| Some n ->
+ (* Print closure of undefined evars *)
str"UNDEFINED EVARS:"++
(if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++
brk(0,1)++
- pr_evar_list sigma (evar_dependency_closure n sigma)++fnl()
+ pr_evar_list sigma (evar_dependency_closure n sigma) ++ fnl()
let pr_evar_by_filter filter sigma =
let open Evd in
@@ -798,7 +799,7 @@ let fold_constr_with_binders sigma g f n acc c =
let iter_constr_with_full_binders g f l c =
let open RelDecl in
- match kind_of_term c with
+ match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> ()
| Cast (c,_, t) -> f l c; f l t
@@ -983,9 +984,9 @@ let isMetaOf sigma mv c =
match EConstr.kind sigma c with Meta mv' -> Int.equal mv mv' | _ -> false
let rec subst_meta bl c =
- match kind_of_term c with
+ match kind c with
| Meta i -> (try Int.List.assoc i bl with Not_found -> c)
- | _ -> map_constr (subst_meta bl) c
+ | _ -> Constr.map (subst_meta bl) c
let rec strip_outer_cast sigma c = match EConstr.kind sigma c with
| Cast (c,_,_) -> strip_outer_cast sigma c
diff --git a/engine/termops.mli b/engine/termops.mli
index ef2c52a455..2dab0685d6 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -10,13 +10,13 @@
needed in the kernel. *)
open Names
-open Term
+open Constr
open Environ
open EConstr
(** printers *)
-val print_sort : sorts -> Pp.t
-val pr_sort_family : sorts_family -> Pp.t
+val print_sort : Sorts.t -> Pp.t
+val pr_sort_family : Sorts.family -> Pp.t
val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
(** about contexts *)
@@ -147,7 +147,7 @@ val subst_term : Evd.evar_map -> constr -> constr -> constr
val replace_term : Evd.evar_map -> constr -> constr -> constr -> constr
(** Alternative term equalities *)
-val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
+val base_sort_cmp : Reduction.conv_pb -> Sorts.t -> Sorts.t -> bool
val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> constr -> constr -> bool) ->
Reduction.conv_pb -> constr -> constr -> bool
val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> constr -> constr -> bool
diff --git a/engine/uState.ml b/engine/uState.ml
index 13a9bb3732..77837fefcf 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -33,10 +33,10 @@ type uinfo = {
(* 2nd part used to check consistency on the fly. *)
type t =
{ uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t;
- uctx_local : Univ.universe_context_set; (** The local context of variables *)
+ uctx_local : Univ.ContextSet.t; (** The local context of variables *)
uctx_univ_variables : Universes.universe_opt_subst;
(** The local universes that are unification variables *)
- uctx_univ_algebraic : Univ.universe_set;
+ uctx_univ_algebraic : Univ.LSet.t;
(** The subset of unification variables that can be instantiated with
algebraic universes as they appear in inferred types only. *)
uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
diff --git a/engine/uState.mli b/engine/uState.mli
index c44f2c1d74..b31e94b285 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -28,13 +28,13 @@ val is_empty : t -> bool
val union : t -> t -> t
-val of_context_set : Univ.universe_context_set -> t
+val of_context_set : Univ.ContextSet.t -> t
val of_binders : Universes.universe_binders -> t
(** {5 Projections} *)
-val context_set : t -> Univ.universe_context_set
+val context_set : t -> Univ.ContextSet.t
(** The local context of the state, i.e. a set of bound variables together
with their associated constraints. *)
@@ -54,7 +54,7 @@ val algebraics : t -> Univ.LSet.t
val constraints : t -> Univ.constraints
(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)
-val context : t -> Univ.universe_context
+val context : t -> Univ.UContext.t
(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
(** {5 Constraints handling} *)
@@ -79,7 +79,7 @@ val universe_of_name : t -> string -> Univ.Level.t
(** {5 Unification} *)
-val restrict : t -> Univ.universe_set -> t
+val restrict : t -> Univ.LSet.t -> t
type rigid =
| UnivRigid
@@ -89,7 +89,7 @@ val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t
+val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> Universes.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
@@ -130,12 +130,12 @@ val normalize : t -> t
Also return the association list of universe names and universes
(including those not in [names]). *)
val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
- (Id.t * Univ.Level.t) list * Univ.universe_context
+ (Id.t * Univ.Level.t) list * Univ.UContext.t
type universe_decl =
(Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
-val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context
+val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.UContext.t
(** {5 TODO: Document me} *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 7f5bf24b74..3136f805c8 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -6,10 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Sorts
open Util
open Pp
open Names
-open Term
+open Constr
open Environ
open Univ
open Globnames
@@ -20,7 +21,7 @@ let pr_with_global_universes l =
(** Local universe names of polymorphic references *)
-type universe_binders = (Id.t * Univ.universe_level) list
+type universe_binders = (Id.t * Univ.Level.t) list
let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders"
@@ -39,7 +40,7 @@ let is_set_minimization () = !set_minimization
type universe_constraint_type = ULe | UEq | ULub
-type universe_constraint = universe * universe_constraint_type * universe
+type universe_constraint = Universe.t * universe_constraint_type * Universe.t
module Constraints = struct
module S = Set.Make(
@@ -157,11 +158,11 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
if res then Some !cstrs else None
let compare_head_gen_proj env equ eqs eqc' m n =
- match kind_of_term m, kind_of_term n with
+ match kind m, kind n with
| Proj (p, c), App (f, args)
| App (f, args), Proj (p, c) ->
- (match kind_of_term f with
- | Const (p', u) when eq_constant (Projection.constant p) p' ->
+ (match kind f with
+ | Const (p', u) when Constant.equal (Projection.constant p) p' ->
let pb = Environ.lookup_projection p env in
let npars = pb.Declarations.proj_npars in
if Array.length args == npars + 1 then
@@ -328,7 +329,7 @@ let fresh_global_or_constr_instance env = function
| IsGlobal gr -> fresh_global_instance env gr
let global_of_constr c =
- match kind_of_term c with
+ match kind c with
| Const (c, u) -> ConstRef c, u
| Ind (i, u) -> IndRef i, u
| Construct (c, u) -> ConstructRef c, u
@@ -390,8 +391,8 @@ let type_of_reference env r =
let type_of_global t = type_of_reference (Global.env ()) t
let fresh_sort_in_family env = function
- | InProp -> prop_sort, ContextSet.empty
- | InSet -> set_sort, ContextSet.empty
+ | InProp -> Sorts.prop, ContextSet.empty
+ | InSet -> Sorts.set, ContextSet.empty
| InType ->
let u = fresh_level () in
Type (Univ.Universe.make u), ContextSet.singleton u
@@ -449,7 +450,7 @@ let nf_evars_and_universes_opt_subst f subst =
let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
let lsubst = Univ.level_subst_of subst in
let rec aux c =
- match kind_of_term c with
+ match kind c with
| Evar (evk, args) ->
let args = Array.map aux args in
(match try f (evk, args) with Not_found -> None with
@@ -467,7 +468,7 @@ let nf_evars_and_universes_opt_subst f subst =
| Sort (Type u) ->
let u' = Univ.subst_univs_universe subst u in
if u' == u then c else mkSort (sort_of_univ u')
- | _ -> map_constr aux c
+ | _ -> Constr.map aux c
in aux
let fresh_universe_context_set_instance ctx =
@@ -526,7 +527,7 @@ let normalize_opt_subst ctx =
else try ignore(normalize u) with Not_found -> assert(false)) ctx
in !ectx
-type universe_opt_subst = universe option universe_map
+type universe_opt_subst = Universe.t option universe_map
let make_opt_subst s =
fun x ->
@@ -788,7 +789,7 @@ let normalize_context_set ctx us algs =
(* We first put constraints in a normal-form: all self-loops are collapsed
to equalities. *)
let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
- ctx UGraph.empty_universes
+ ctx UGraph.initial_universes
in
let g =
Univ.Constraint.fold
diff --git a/engine/universes.mli b/engine/universes.mli
index 8b2217d446..24613c4b91 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -8,7 +8,7 @@
open Util
open Names
-open Term
+open Constr
open Environ
open Univ
@@ -21,26 +21,26 @@ val pr_with_global_universes : Level.t -> Pp.t
(** Local universe name <-> level mapping *)
-type universe_binders = (Id.t * Univ.universe_level) list
-
+type universe_binders = (Id.t * Univ.Level.t) list
+
val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
val universe_binders_of_global : Globnames.global_reference -> universe_binders
(** The global universe counter *)
-val set_remote_new_univ_level : universe_level RemoteCounter.installer
+val set_remote_new_univ_level : Level.t RemoteCounter.installer
(** Side-effecting functions creating new universe levels. *)
-val new_univ_level : Names.dir_path -> universe_level
-val new_univ : Names.dir_path -> universe
-val new_Type : Names.dir_path -> types
-val new_Type_sort : Names.dir_path -> sorts
+val new_univ_level : DirPath.t -> Level.t
+val new_univ : DirPath.t -> Universe.t
+val new_Type : DirPath.t -> types
+val new_Type_sort : DirPath.t -> Sorts.t
-val new_global_univ : unit -> universe in_universe_context_set
-val new_sort_in_family : sorts_family -> sorts
+val new_global_univ : unit -> Universe.t in_universe_context_set
+val new_sort_in_family : Sorts.family -> Sorts.t
(** {6 Constraints for type inference}
-
+
When doing conversion of universes, not only do we have =/<= constraints but
also Lub constraints which correspond to unification of two levels which might
not be necessary if unfolding is performed.
@@ -48,7 +48,7 @@ val new_sort_in_family : sorts_family -> sorts
type universe_constraint_type = ULe | UEq | ULub
-type universe_constraint = universe * universe_constraint_type * universe
+type universe_constraint = Universe.t * universe_constraint_type * Universe.t
module Constraints : sig
include Set.S with type elt = universe_constraint
@@ -63,7 +63,7 @@ type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> unive
val subst_univs_universe_constraints : universe_subst_fn ->
universe_constraints -> universe_constraints
-val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
+val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function
val to_constraints : UGraph.t -> universe_constraints -> constraints
@@ -82,15 +82,15 @@ val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrai
(** Build a fresh instance for a given context, its associated substitution and
the instantiated constraints. *)
-val fresh_instance_from_context : abstract_universe_context ->
- universe_instance constrained
+val fresh_instance_from_context : AUContext.t ->
+ Instance.t constrained
-val fresh_instance_from : abstract_universe_context -> universe_instance option ->
- universe_instance in_universe_context_set
+val fresh_instance_from : AUContext.t -> Instance.t option ->
+ Instance.t in_universe_context_set
-val fresh_sort_in_family : env -> sorts_family ->
- sorts in_universe_context_set
-val fresh_constant_instance : env -> constant ->
+val fresh_sort_in_family : env -> Sorts.family ->
+ Sorts.t in_universe_context_set
+val fresh_constant_instance : env -> Constant.t ->
pconstant in_universe_context_set
val fresh_inductive_instance : env -> inductive ->
pinductive in_universe_context_set
@@ -105,15 +105,15 @@ val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_const
(** Get fresh variables for the universe context.
Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : universe_context_set ->
- universe_level_subst * universe_context_set
+val fresh_universe_context_set_instance : ContextSet.t ->
+ universe_level_subst * ContextSet.t
(** Raises [Not_found] if not a global reference. *)
val global_of_constr : constr -> Globnames.global_reference puniverses
val constr_of_global_univ : Globnames.global_reference puniverses -> constr
-val extend_context : 'a in_universe_context_set -> universe_context_set ->
+val extend_context : 'a in_universe_context_set -> ContextSet.t ->
'a in_universe_context_set
(** Simplification and pruning of constraints:
@@ -127,38 +127,38 @@ val extend_context : 'a in_universe_context_set -> universe_context_set ->
(a global one if there is one) and transitively saturate
the constraints w.r.t to the equalities. *)
-module UF : Unionfind.PartitionSig with type elt = universe_level
+module UF : Unionfind.PartitionSig with type elt = Level.t
-type universe_opt_subst = universe option universe_map
+type universe_opt_subst = Universe.t option universe_map
val make_opt_subst : universe_opt_subst -> universe_subst_fn
val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
-val normalize_context_set : universe_context_set ->
+val normalize_context_set : ContextSet.t ->
universe_opt_subst (* The defined and undefined variables *) ->
- universe_set (* univ variables that can be substituted by algebraics *) ->
- (universe_opt_subst * universe_set) in_universe_context_set
+ LSet.t (* univ variables that can be substituted by algebraics *) ->
+ (universe_opt_subst * LSet.t) in_universe_context_set
val normalize_univ_variables : universe_opt_subst ->
- universe_opt_subst * universe_set * universe_set * universe_subst
+ universe_opt_subst * LSet.t * LSet.t * universe_subst
val normalize_univ_variable :
- find:(universe_level -> universe) ->
- update:(universe_level -> universe -> universe) ->
- universe_level -> universe
+ find:(Level.t -> Universe.t) ->
+ update:(Level.t -> Universe.t -> Universe.t) ->
+ Level.t -> Universe.t
val normalize_univ_variable_opt_subst : universe_opt_subst ref ->
- (universe_level -> universe)
+ (Level.t -> Universe.t)
val normalize_univ_variable_subst : universe_subst ref ->
- (universe_level -> universe)
+ (Level.t -> Universe.t)
val normalize_universe_opt_subst : universe_opt_subst ref ->
- (universe -> universe)
+ (Universe.t -> Universe.t)
val normalize_universe_subst : universe_subst ref ->
- (universe -> universe)
+ (Universe.t -> Universe.t)
(** Create a fresh global in the global environment, without side effects.
BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
@@ -180,7 +180,7 @@ val type_of_global : Globnames.global_reference -> types in_universe_context_set
val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
universe_opt_subst -> constr -> constr
-val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t
+val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t
(** Pretty-printing *)
@@ -188,11 +188,11 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t
(** {6 Support for template polymorphism } *)
-val solve_constraints_system : universe option array -> universe array -> universe array ->
- universe array
+val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
+ Universe.t array
(** Operations for universe_info_ind *)
(** Given a universe context representing constraints of an inductive
this function produces a UInfoInd.t that with the trivial subtyping relation. *)
-val univ_inf_ind_from_universe_context : universe_context -> cumulativity_info
+val univ_inf_ind_from_universe_context : UContext.t -> CumulativityInfo.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 22:48:59 +0000