aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml1
-rw-r--r--engine/evarutil.ml16
-rw-r--r--engine/evd.ml14
-rw-r--r--engine/evd.mli4
-rw-r--r--engine/ftactic.ml4
-rw-r--r--engine/logic_monad.ml2
-rw-r--r--engine/logic_monad.mli5
-rw-r--r--engine/namegen.ml2
-rw-r--r--engine/nameops.mli1
-rw-r--r--engine/proofview.ml14
-rw-r--r--engine/proofview.mli7
-rw-r--r--engine/termops.ml22
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml14
-rw-r--r--engine/uState.mli2
-rw-r--r--engine/univGen.ml21
-rw-r--r--engine/univGen.mli10
-rw-r--r--engine/univMinim.ml15
-rw-r--r--engine/univNames.ml22
-rw-r--r--engine/univNames.mli2
20 files changed, 97 insertions, 83 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 96f1ce5e60..24d161d00a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -606,6 +606,7 @@ let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
let subst_univs_level_constr subst c =
of_constr (Vars.subst_univs_level_constr subst (to_constr c))
+
(** Operations that dot NOT commute with evar-normalization *)
let noccurn sigma n term =
let rec occur_rec n c = match kind sigma c with
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 69ee5223c4..db56d0628f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -155,7 +155,7 @@ let is_ground_env = memo is_ground_env
exception NoHeadEvar
let head_evar sigma c =
- (** FIXME: this breaks if using evar-insensitive code *)
+ (* FIXME: this breaks if using evar-insensitive code *)
let c = EConstr.Unsafe.to_constr c in
let rec hrec c = match kind c with
| Evar (evk,_) -> evk
@@ -288,7 +288,7 @@ let empty_csubst = {
}
let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c =
- (** Safe because this is a substitution *)
+ (* Safe because this is a substitution *)
let c = EConstr.Unsafe.to_constr c in
let rec subst n c = match Constr.kind c with
| Rel m ->
@@ -318,7 +318,7 @@ let update_var src tgt subst =
in
match cur with
| None ->
- (** Missing keys stand for identity substitution [src ↦ src] *)
+ (* Missing keys stand for identity substitution [src ↦ src] *)
let csubst_var = Id.Map.add src (Constr.mkVar tgt) subst.csubst_var in
let csubst_rev = Id.Map.add tgt (SVar src) subst.csubst_rev in
{ subst with csubst_var; csubst_rev }
@@ -366,8 +366,8 @@ let push_rel_decl_to_named_context
about this whole name generation problem. *)
if Flags.is_program_mode () then next_name_away na avoid
else
- (** id_of_name_using_hdchar only depends on the rel context which is empty
- here *)
+ (* id_of_name_using_hdchar only depends on the rel context which is empty
+ here *)
next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid
in
match extract_if_neq id na with
@@ -540,8 +540,8 @@ let restrict_evar evd evk filter ?src candidates =
| Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None))
| _ ->
let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
- (** Mark new evar as future goal, removing previous one,
- circumventing Proofview.advance but making Proof.run_tactic catch these. *)
+ (* Mark new evar as future goal, removing previous one,
+ circumventing Proofview.advance but making Proof.run_tactic catch these. *)
let future_goals = Evd.save_future_goals evd in
let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in
let evd = Evd.restore_future_goals evd future_goals in
@@ -779,7 +779,7 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with
let r =
try Id.Map.find id cache.cache
with Not_found ->
- (** Dummy value *)
+ (* Dummy value *)
let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
let () = cache.cache <- Id.Map.add id r cache.cache in
r
diff --git a/engine/evd.ml b/engine/evd.ml
index 6345046431..7bc3be87a4 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -89,8 +89,8 @@ struct
| Some f2 -> normalize (CList.filter_with f1 f2)
let apply_subfilter_array filter subfilter =
- (** In both cases we statically know that the argument will contain at
- least one [false] *)
+ (* In both cases we statically know that the argument will contain at
+ least one [false] *)
match filter with
| None -> Some (Array.to_list subfilter)
| Some f ->
@@ -395,7 +395,7 @@ let rename evk id (evtoid, idtoev) =
let reassign_name_defined evk evk' (evtoid, idtoev as names) =
let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
match id with
- | None -> names (** evk' must not be defined *)
+ | None -> names (* evk' must not be defined *)
| Some id ->
(EvMap.add evk' id (EvMap.remove evk evtoid),
Id.Map.add id evk' (Id.Map.remove id idtoev))
@@ -416,7 +416,7 @@ type evar_flags =
typeclass_evars : Evar.Set.t }
type evar_map = {
- (** Existential variables *)
+ (* Existential variables *)
defn_evars : evar_info EvMap.t;
undf_evars : evar_info EvMap.t;
evar_names : EvNames.t;
@@ -520,7 +520,7 @@ let inherit_evar_flags evar_flags evk evk' =
let remove_evar_flags evk evar_flags =
{ typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
- (** Restriction information is kept. *)
+ (* Restriction information is kept. *)
restricted_evars = evar_flags.restricted_evars }
(** New evars *)
@@ -1341,14 +1341,14 @@ module MiniEConstr = struct
| None -> c
end
| App (f, args) when isEvar f ->
- (** Enforce smart constructor invariant on applications *)
+ (* Enforce smart constructor invariant on applications *)
let ev = 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 ->
- (** Enforce smart constructor invariant on casts. *)
+ (* Enforce smart constructor invariant on casts. *)
let ev = destEvar c0 in
begin match safe_evar_value sigma ev with
| None -> c
diff --git a/engine/evd.mli b/engine/evd.mli
index 0a8d1f3287..7560d68805 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -86,7 +86,7 @@ type evar_body =
type evar_info = {
evar_concl : econstr;
(** Type of the evar. *)
- evar_hyps : named_context_val; (** TODO econstr? *)
+ evar_hyps : named_context_val; (* TODO econstr? *)
(** Context of the evar. *)
evar_body : evar_body;
(** Optional content of the evar. *)
@@ -546,6 +546,7 @@ val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * UState.t
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
@@ -567,6 +568,7 @@ val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map
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.Level.t -> Univ.Level.t *)
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index b371884ba4..ac0344148a 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -29,8 +29,8 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
| Depends l ->
let f arg = f arg >>= function
| Uniform x ->
- (** We dispatch the uniform result on each goal under focus, as we know
- that the [m] argument was actually dependent. *)
+ (* We dispatch the uniform result on each goal under focus, as we know
+ that the [m] argument was actually dependent. *)
Proofview.Goal.goals >>= fun goals ->
let ans = List.map (fun g -> (g,x)) goals in
Proofview.tclUNIT ans
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 4afa817b27..e0c24f049f 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -28,8 +28,10 @@
from the IO monad ([Proofview] catches errors in its compatibility
layer, and when lifting goal-level expressions). *)
exception Exception of exn
+
(** This exception is used to signal abortion in [timeout] functions. *)
exception Timeout
+
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
interrupts). *)
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 545334ce9a..3e57baab26 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -28,8 +28,10 @@
from the IO monad ([Proofview] catches errors in its compatibility
layer, and when lifting goal-level expressions). *)
exception Exception of exn
+
(** This exception is used to signal abortion in [timeout] functions. *)
exception Timeout
+
(** This exception is used by the tactics to signal failure by lack of
successes, rather than some other exceptions (like system
interrupts). *)
@@ -51,8 +53,10 @@ module NonLogical : sig
val ref : 'a -> 'a ref t
(** [Pervasives.(:=)] *)
+
val (:=) : 'a ref -> 'a -> unit t
(** [Pervasives.(!)] *)
+
val (!) : 'a ref -> 'a t
val read_line : string t
@@ -67,6 +71,7 @@ module NonLogical : sig
(** [Pervasives.raise]. Except that exceptions are wrapped with
{!Exception}. *)
val raise : ?info:Exninfo.info -> exn -> 'a t
+
(** [try ... with ...] but restricted to {!Exception}. *)
val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
val timeout : int -> 'a t -> 'a t
diff --git a/engine/namegen.ml b/engine/namegen.ml
index a67ff6965b..018eca1ba2 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -358,7 +358,7 @@ let next_name_away_with_default_using_types default na avoid t =
let next_name_away = next_name_away_with_default default_non_dependent_string
let make_all_name_different env sigma =
- (** FIXME: this is inefficient, but only used in printing *)
+ (* FIXME: this is inefficient, but only used in printing *)
let avoid = ref (ids_of_named_context_val (named_context_val env)) in
let sign = named_context_val env in
let rels = rel_context env in
diff --git a/engine/nameops.mli b/engine/nameops.mli
index 8a93fad8cc..a5308904f5 100644
--- a/engine/nameops.mli
+++ b/engine/nameops.mli
@@ -16,6 +16,7 @@ val make_ident : string -> int option -> Id.t
val repr_ident : Id.t -> string * int option
val atompart_of_id : Id.t -> string (** remove trailing digits *)
+
val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)
val add_suffix : Id.t -> string -> Id.t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 304b2dff84..8c15579bb0 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -660,9 +660,9 @@ let unifiable_delayed g l =
let free_evars sigma l =
let cache = Evarutil.create_undefined_evars_cache () in
let map ev =
- (** Computes the set of evars appearing in the hypotheses, the conclusion or
- the body of the evar_info [evi]. Note: since we want to use it on goals,
- the body is actually supposed to be empty. *)
+ (* Computes the set of evars appearing in the hypotheses, the conclusion or
+ the body of the evar_info [evi]. Note: since we want to use it on goals,
+ the body is actually supposed to be empty. *)
let evi = Evd.find sigma ev in
let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
(ev, fevs)
@@ -672,9 +672,9 @@ let free_evars sigma l =
let free_evars_with_state sigma l =
let cache = Evarutil.create_undefined_evars_cache () in
let map ev =
- (** Computes the set of evars appearing in the hypotheses, the conclusion or
- the body of the evar_info [evi]. Note: since we want to use it on goals,
- the body is actually supposed to be empty. *)
+ (* Computes the set of evars appearing in the hypotheses, the conclusion or
+ the body of the evar_info [evi]. Note: since we want to use it on goals,
+ the body is actually supposed to be empty. *)
let ev = drop_state ev in
let evi = Evd.find sigma ev in
let fevs = lazy (Evarutil.filtered_undefined_evars_of_evar_info ~cache sigma evi) in
@@ -1157,7 +1157,7 @@ module Goal = struct
let sigma = step.solution in
let map goal =
match cleared_alias sigma goal with
- | None -> None (** ppedrot: Is this check really necessary? *)
+ | None -> None (* ppedrot: Is this check really necessary? *)
| Some goal ->
let gl =
Env.get >>= fun env ->
diff --git a/engine/proofview.mli b/engine/proofview.mli
index cda4808a23..28e793f0fc 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -398,6 +398,7 @@ val tclPROGRESS : 'a tactic -> 'a tactic
val tclCHECKINTERRUPT : unit tactic
exception Timeout
+
(** [tclTIMEOUT n t] can have only one success.
In case of timeout if fails with [tclZERO Timeout]. *)
val tclTIMEOUT : int -> 'a tactic -> 'a tactic
@@ -517,8 +518,8 @@ module Goal : sig
(** Like {!nf_enter}, but does not normalize the goal beforehand. *)
val enter : (t -> unit tactic) -> unit tactic
- (** Like {!enter}, but assumes exactly one goal under focus, raising *)
- (** a fatal error otherwise. *)
+ (** Like {!enter}, but assumes exactly one goal under focus, raising
+ a fatal error otherwise. *)
val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic
(** Recover the list of current goals under focus, without evar-normalization.
@@ -612,8 +613,10 @@ module Notations : sig
(** {!tclBIND} *)
val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+
(** {!tclTHEN} *)
val (<*>) : unit tactic -> 'a tactic -> 'a tactic
+
(** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
diff --git a/engine/termops.ml b/engine/termops.ml
index 98300764df..137770d8f0 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -197,8 +197,8 @@ let compute_evar_dependency_graph sigma =
let evar_dependency_closure n sigma =
let open Evd in
- (** Create the DAG of depth [n] representing the recursive dependencies of
- undefined evars. *)
+ (* Create the DAG of depth [n] representing the recursive dependencies of
+ undefined evars. *)
let graph = compute_evar_dependency_graph sigma in
let rec aux n curr accu =
if Int.equal n 0 then Evar.Set.union curr accu
@@ -209,9 +209,9 @@ let evar_dependency_closure n sigma =
Evar.Set.union deps accu
with Not_found -> accu
in
- (** Consider only the newly added evars *)
+ (* Consider only the newly added evars *)
let ncurr = Evar.Set.fold fold curr Evar.Set.empty in
- (** Merge the others *)
+ (* Merge the others *)
let accu = Evar.Set.union curr accu in
aux (n - 1) ncurr accu
in
@@ -261,13 +261,13 @@ let print_env_short env sigma =
let pr_evar_constraints sigma pbs =
let pr_evconstr (pbty, env, t1, t2) =
let env =
- (** We currently allow evar instances to refer to anonymous de
- Bruijn indices, so we protect the error printing code in this
- case by giving names to every de Bruijn variable in the
- rel_context of the conversion problem. MS: we should rather
- stop depending on anonymous variables, they can be used to
- indicate independency. Also, this depends on a strategy for
- naming/renaming. *)
+ (* We currently allow evar instances to refer to anonymous de
+ Bruijn indices, so we protect the error printing code in this
+ case by giving names to every de Bruijn variable in the
+ rel_context of the conversion problem. MS: we should rather
+ stop depending on anonymous variables, they can be used to
+ indicate independency. Also, this depends on a strategy for
+ naming/renaming. *)
Namegen.make_all_name_different env sigma
in
print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++
diff --git a/engine/termops.mli b/engine/termops.mli
index eef8452e64..7920af8e0e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -290,7 +290,7 @@ val is_Prop : Evd.evar_map -> constr -> bool
val is_Set : Evd.evar_map -> constr -> bool
val is_Type : Evd.evar_map -> constr -> bool
-val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid
+val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
(** Combinators on judgments *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 6aecc368e6..6969d2ba44 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -197,7 +197,7 @@ let process_universe_constraints ctx cstrs =
| Some l -> Inr l
in
let equalize_variables fo l l' r r' local =
- (** Assumes l = [l',0] and r = [r',0] *)
+ (* Assumes l = [l',0] and r = [r',0] *)
let () =
if is_local l' then
instantiate_variable l' r vars
@@ -235,8 +235,8 @@ let process_universe_constraints ctx cstrs =
match cst with
| ULe (l, r) ->
if UGraph.check_leq univs l r then
- (** Keep Prop/Set <= var around if var might be instantiated by prop or set
- later. *)
+ (* Keep Prop/Set <= var around if var might be instantiated by prop or set
+ later. *)
match Univ.Universe.level l, Univ.Universe.level r with
| Some l, Some r ->
Univ.Constraint.add (l, Univ.Le, r) local
@@ -324,12 +324,14 @@ let constrain_variables diff ctx =
let qualid_of_level uctx =
let map, map_rev = uctx.uctx_names in
fun l ->
- try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)
+ try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname))
with Not_found | Option.IsNone ->
UnivNames.qualid_of_level l
let pr_uctx_level uctx l =
- Libnames.pr_qualid (qualid_of_level uctx l)
+ match qualid_of_level uctx l with
+ | Some qid -> Libnames.pr_qualid qid
+ | None -> Univ.Level.pr l
type ('a, 'b) gen_universe_decl = {
univdecl_instance : 'a; (* Declared universes *)
@@ -533,7 +535,7 @@ let emit_side_effects eff u =
let new_univ_variable ?loc rigid name
({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
- let u = UnivGen.new_univ_level () in
+ let u = UnivGen.fresh_level () in
let ctx' = Univ.ContextSet.add_universe u ctx in
let uctx', pred =
match rigid with
diff --git a/engine/uState.mli b/engine/uState.mli
index ad0cd5c1bb..5170184ef4 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -188,6 +188,6 @@ val update_sigma_env : t -> Environ.env -> t
(** {5 Pretty-printing} *)
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
-val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid
+val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 130aa06f53..40c4c909fe 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,26 +13,25 @@ open Names
open Constr
open Univ
+type univ_unique_id = int
(* Generator of levels *)
-type universe_id = DirPath.t * int
-
let new_univ_id, set_remote_new_univ_id =
RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
- ~build:(fun n -> Global.current_dirpath (), n)
+ ~build:(fun n -> n)
-let new_univ_level () =
- let dp, id = new_univ_id () in
- Univ.Level.make dp id
+let new_univ_global () =
+ Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
-let fresh_level () = new_univ_level ()
+let fresh_level () =
+ Univ.Level.make (new_univ_global ())
(* TODO: remove *)
-let new_univ dp = Univ.Universe.make (new_univ_level dp)
-let new_Type dp = mkType (new_univ dp)
-let new_Type_sort dp = Type (new_univ dp)
+let new_univ () = Univ.Universe.make (fresh_level ())
+let new_Type () = mkType (new_univ ())
+let new_Type_sort () = Type (new_univ ())
let fresh_instance auctx =
- let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+ let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
let ctx = Array.fold_right LSet.add inst LSet.empty in
let inst = Instance.of_array inst in
inst, (ctx, AUContext.instantiate inst auctx)
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 8af5f8fdb0..b4598e10d0 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -15,14 +15,14 @@ open Univ
(** The global universe counter *)
-type universe_id = DirPath.t * int
-
-val set_remote_new_univ_id : universe_id RemoteCounter.installer
+type univ_unique_id
+val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer
+val new_univ_id : unit -> univ_unique_id (** for the stm *)
(** Side-effecting functions creating new universe levels. *)
-val new_univ_id : unit -> universe_id
-val new_univ_level : unit -> Level.t
+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]"]
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index e20055b133..1619ac3d34 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -32,15 +32,15 @@ let add_list_map u t map =
let choose_canonical ctx flexible algs s =
let global = LSet.diff s ctx in
let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in
- (** If there is a global universe in the set, choose it *)
+ (* If there is a global universe in the set, choose it *)
if not (LSet.is_empty global) then
let canon = LSet.choose global in
canon, (LSet.remove canon global, rigid, flexible)
- else (** No global in the equivalence class, choose a rigid one *)
+ else (* No global in the equivalence class, choose a rigid one *)
if not (LSet.is_empty rigid) then
let canon = LSet.choose rigid in
canon, (global, LSet.remove canon rigid, flexible)
- else (** There are only flexible universes in the equivalence
+ else (* There are only flexible universes in the equivalence
class, choose a non-algebraic. *)
let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in
if not (LSet.is_empty nonalgs) then
@@ -94,8 +94,8 @@ let find_inst insts v =
with Found (f,l) -> (f,l)
let compute_lbound left =
- (** The universe variable was not fixed yet.
- Compute its level using its lower bound. *)
+ (* The universe variable was not fixed yet.
+ Compute its level using its lower bound. *)
let sup l lbound =
match lbound with
| None -> Some l
@@ -154,9 +154,10 @@ let not_lower lower (d,l) =
* constraints we must keep it. *)
compare_constraint_type d d' > 0
with Not_found ->
- (** No constraint existing on l *) true) l
+ (* No constraint existing on l *) true) l
exception UpperBoundedAlg
+
(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper
constraints to [lbound], adding them to [cstrs].
@@ -269,7 +270,7 @@ module UPairSet = Set.Make (UPairs)
let normalize_context_set g ctx us algs weak =
let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
- (** Keep the Prop/Set <= i constraints separate for minimization *)
+ (* Keep the Prop/Set <= i constraints separate for minimization *)
let smallles, csts =
Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
in
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 1019f8f0c2..7e6ed5e4c0 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -15,17 +15,15 @@ open Univ
let qualid_of_level l =
match Level.name l with
- | Some (d, n as na) ->
- begin
- try Nametab.shortest_qualid_of_universe na
- with Not_found ->
- let name = Id.of_string_soft (string_of_int n) in
- Libnames.make_qualid d name
- end
- | None ->
- Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l)
+ | Some qid ->
+ (try Some (Nametab.shortest_qualid_of_universe qid)
+ with Not_found -> None)
+ | None -> None
-let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l)
+let pr_with_global_universes l =
+ match qualid_of_level l with
+ | Some qid -> Libnames.pr_qualid qid
+ | None -> Level.pr l
(** Global universe information outside the kernel, to handle
polymorphic universe names in sections that have to be discharged. *)
@@ -37,8 +35,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
let empty_binders = Id.Map.empty
let name_universe lvl =
- (** Best-effort naming from the string representation of the level. This is
- completely hackish and should be solved in upper layers instead. *)
+ (* Best-effort naming from the string representation of the level. This is
+ completely hackish and should be solved in upper layers instead. *)
Id.of_string_soft (Level.to_string lvl)
let compute_instance_binders inst ubinders =
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 6e68153ac2..e9c517babf 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -11,7 +11,7 @@
open Univ
val pr_with_global_universes : Level.t -> Pp.t
-val qualid_of_level : Level.t -> Libnames.qualid
+val qualid_of_level : Level.t -> Libnames.qualid option
(** Local universe name <-> level mapping *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 11:36:26 +0000