aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml4
-rw-r--r--library/declare.mli14
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/global.ml2
-rw-r--r--library/globnames.ml2
-rw-r--r--library/goptions.ml6
-rw-r--r--library/heads.ml2
-rw-r--r--library/impargs.ml13
-rw-r--r--library/impargs.mli12
-rw-r--r--library/kindops.ml4
-rw-r--r--library/lib.ml32
-rw-r--r--library/lib.mli9
-rw-r--r--library/libnames.ml2
-rw-r--r--library/libobject.ml6
-rw-r--r--library/library.ml28
-rw-r--r--library/loadpath.ml5
-rw-r--r--library/nametab.ml2
-rw-r--r--library/states.ml2
-rw-r--r--library/summary.ml35
-rw-r--r--library/summary.mli11
-rw-r--r--library/universes.ml4
21 files changed, 95 insertions, 104 deletions
diff --git a/library/declare.ml b/library/declare.ml
index f809e97423..3d063225f4 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -9,7 +9,7 @@
(** This module is about the low-level declaration of logical objects *)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Libnames
@@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) =
obj.cst_was_seff <- false;
if Global.exists_objlabel (Label.of_id (basename sp))
then constant_of_kn kn
- else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+ else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
end else
let () = check_exists sp in
let kn', exported = Global.add_constant dir id obj.cst_decl in
diff --git a/library/declare.mli b/library/declare.mli
index 8dd24d2780..7824506da0 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,14 +34,6 @@ val declare_variable : variable -> variable_declaration -> object_name
type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
-(** [declare_constant id cd] declares a global declaration
- (constant/parameter) with name [id] in the current section; it returns
- the full path of the declaration
-
- internal specify if the constant has been created by the kernel or by the
- user, and in the former case, if its errors should be silent
-
- *)
type internal_flag =
| UserAutomaticRequest
| InternalTacticRequest
@@ -53,6 +45,12 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
?poly:polymorphic -> ?univs:Univ.universe_context ->
?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
+(** [declare_constant id cd] declares a global declaration
+ (constant/parameter) with name [id] in the current section; it returns
+ the full path of the declaration
+
+ internal specify if the constant has been created by the kernel or by the
+ user, and in the former case, if its errors should be silent *)
val declare_constant :
?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
diff --git a/library/declaremods.ml b/library/declaremods.ml
index dcd63c7691..b2806a1ac3 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Declarations
@@ -822,7 +822,7 @@ let protect_summaries f =
try f fs
with reraise ->
(* Something wrong: undo the whole process *)
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = Summary.unfreeze_summaries fs in
iraise reraise
diff --git a/library/global.ml b/library/global.ml
index c536119314..e748434d24 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -42,7 +42,7 @@ let () =
let assert_not_parsing () =
if !Flags.we_are_parsing then
- Errors.anomaly (
+ CErrors.anomaly (
Pp.strbrk"The global environment cannot be accessed during parsing")
let safe_env () = assert_not_parsing(); !global_env
diff --git a/library/globnames.ml b/library/globnames.ml
index bec463ecf2..a78f5f13a9 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Names
open Term
open Mod_subst
diff --git a/library/goptions.ml b/library/goptions.ml
index 7bead0b63d..1cf25987b1 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -9,7 +9,7 @@
(* This module manages customization parameters at the vernacular level *)
open Pp
-open Errors
+open CErrors
open Util
open Libobject
open Libnames
@@ -365,8 +365,8 @@ let set_string_option_value = set_string_option_value_gen None
let msg_option_value (name,v) =
match v with
- | BoolValue true -> str "true"
- | BoolValue false -> str "false"
+ | BoolValue true -> str "on"
+ | BoolValue false -> str "off"
| IntValue (Some n) -> int n
| IntValue None -> str "undefined"
| StringValue s -> str s
diff --git a/library/heads.ml b/library/heads.ml
index 4c9b789769..02465f22fc 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -70,7 +70,7 @@ let kind_of_head env t =
| Const (cst,_) ->
(try on_subterm k l b (constant_head cst)
with Not_found ->
- Errors.anomaly
+ CErrors.anomaly
Pp.(str "constant not found in kind_of_head: " ++
str (Names.Constant.to_string cst)))
| Construct _ | CoFix _ ->
diff --git a/library/impargs.ml b/library/impargs.ml
index feb3bf0187..bce7a15cbe 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Globnames
@@ -68,15 +68,14 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
let is_contextual_implicit_args () = !implicit_args.contextual
let is_maximal_implicit_args () = !implicit_args.maximal
-let with_implicits flags f x =
+let with_implicit_protection f x =
let oflags = !implicit_args in
try
- implicit_args := flags;
let rslt = f x in
implicit_args := oflags;
rslt
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = implicit_args := oflags in
iraise reraise
@@ -188,7 +187,7 @@ let is_reversible_pattern bound depth f l =
(* Precondition: rels in env are for inductive types only *)
let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
let rec frec rig (env,depth as ed) c =
- let hd = if strict then whd_betadeltaiota env c else c in
+ let hd = if strict then whd_all env c else c in
let c = if strongly_strict then hd else c in
match kind_of_term hd with
| Rel n when (n < bound+depth) && (n >= depth) ->
@@ -236,7 +235,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
let rigid = ref true in
let open Context.Rel.Declaration in
let rec aux env avoid n names t =
- let t = whd_betadeltaiota env t in
+ let t = whd_all env t in
match kind_of_term t with
| Prod (na,a,b) ->
let na',avoid' = find_displayed_name_in all avoid na (names,b) in
@@ -250,7 +249,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
add_free_rels_until strict strongly_strict revpat n env t Conclusion v
else v
in
- match kind_of_term (whd_betadeltaiota env t) with
+ match kind_of_term (whd_all env t) with
| Prod (na,a,b) ->
let na',avoid = find_displayed_name_in all [] na ([],b) in
let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
diff --git a/library/impargs.mli b/library/impargs.mli
index 34e529ca2c..3919a519c9 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool
val is_contextual_implicit_args : unit -> bool
val is_maximal_implicit_args : unit -> bool
-type implicits_flags
-val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
+val with_implicit_protection : ('a -> 'b) -> 'a -> 'b
(** {6 ... } *)
(** An [implicits_list] is a list of positions telling which arguments
@@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list
val select_stronger_impargs : implicits_list list -> implicit_status list
-type implicit_interactive_request
-
-type implicit_discharge_request =
- | ImplLocal
- | ImplConstant of constant * implicits_flags
- | ImplMutualInductive of mutual_inductive * implicits_flags
- | ImplInteractive of global_reference * implicits_flags *
- implicit_interactive_request
-
val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
(** Equality on [explicitation]. *)
diff --git a/library/kindops.ml b/library/kindops.ml
index c634193da8..21b1bec33c 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -25,7 +25,7 @@ let string_of_theorem_kind = function
let string_of_definition_kind def =
let (locality, poly, kind) = def in
- let error () = Errors.anomaly (Pp.str "Internal definition kind") in
+ let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
match kind with
| Definition ->
begin match locality with
@@ -64,4 +64,4 @@ let string_of_definition_kind def =
| Global -> "Global Instance"
end
| (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
- Errors.anomaly (Pp.str "Internal definition kind")
+ CErrors.anomaly (Pp.str "Internal definition kind")
diff --git a/library/lib.ml b/library/lib.ml
index 23a2d4846d..7218950da3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Libnames
open Globnames
@@ -506,13 +506,6 @@ let section_instance = function
let is_in_section ref =
try ignore (section_instance ref); true with Not_found -> false
-let full_replacement_context () = List.map pi2 !sectab
-let full_section_segment_of_constant con =
- List.map (fun (vars,_,(x,_)) -> fun hyps ->
- named_of_variable_context
- (try pi1 (Names.Cmap.find con x)
- with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab
-
(*************)
(* Sections. *)
@@ -613,15 +606,6 @@ let rec dp_of_mp = function
|Names.MPbound _ -> library_dp ()
|Names.MPdot (mp,_) -> dp_of_mp mp
-let rec split_mp = function
- |Names.MPfile dp -> dp, Names.DirPath.empty
- |Names.MPdot (prfx, lbl) ->
- let mprec, dprec = split_mp prfx in
- mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl)
- |Names.MPbound mbid ->
- let (_,id,dp) = Names.MBId.repr mbid in
- library_dp (), Names.DirPath.make [id]
-
let rec split_modpath = function
|Names.MPfile dp -> dp, []
|Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid]
@@ -633,20 +617,6 @@ let library_part = function
|VarRef id -> library_dp ()
|ref -> dp_of_mp (mp_of_global ref)
-let remove_section_part ref =
- let sp = Nametab.path_of_global ref in
- let dir,_ = repr_path sp in
- match ref with
- | VarRef id ->
- anomaly (Pp.str "remove_section_part not supported on local variables")
- | _ ->
- if is_dirpath_prefix_of dir (cwd ()) then
- (* Not yet (fully) discharged *)
- pop_dirpath_n (sections_depth ()) (cwd ())
- else
- (* Theorem/Lemma outside its outer section of definition *)
- dir
-
(************************)
(* Discharging names *)
diff --git a/library/lib.mli b/library/lib.mli
index 7080b5dba7..0a70152efb 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -138,10 +138,8 @@ val library_dp : unit -> Names.DirPath.t
(** Extract the library part of a name even if in a section *)
val dp_of_mp : Names.module_path -> Names.DirPath.t
-val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t
val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list
val library_part : Globnames.global_reference -> Names.DirPath.t
-val remove_section_part : Globnames.global_reference -> Names.DirPath.t
(** {6 Sections } *)
@@ -191,10 +189,3 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive
val discharge_con : Names.constant -> Names.constant
val discharge_global : Globnames.global_reference -> Globnames.global_reference
val discharge_inductive : Names.inductive -> Names.inductive
-
-(* discharging a constant in one go *)
-val full_replacement_context : unit -> Opaqueproof.work_list list
-val full_section_segment_of_constant :
- Names.constant -> (Context.Named.t -> Context.Named.t) list
-
-
diff --git a/library/libnames.ml b/library/libnames.ml
index 99ff2f2fb4..dd74e192ff 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
diff --git a/library/libobject.ml b/library/libobject.ml
index 3e08b38b12..caa03c85be 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -31,7 +31,7 @@ let default_object s = {
load_function = (fun _ _ -> ());
open_function = (fun _ _ -> ());
subst_function = (fun _ ->
- Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
+ CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
classify_function = (fun obj -> Keep obj);
discharge_function = (fun _ -> None);
rebuild_function = (fun x -> x)}
@@ -97,10 +97,10 @@ let declare_object_full odecl =
let declare_object odecl =
try fst (declare_object_full odecl)
- with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
+ with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
let declare_object_full odecl =
try declare_object_full odecl
- with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
+ with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
(* this function describes how the cache, load, open, and export functions
are triggered. *)
diff --git a/library/library.ml b/library/library.ml
index cead907009..d44f796a7a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
@@ -64,7 +64,7 @@ let fetch_delayed del =
let () = close_in ch in
if not (String.equal digest digest') then raise (Faulty f);
obj
- with e when Errors.noncritical e -> raise (Faulty f)
+ with e when CErrors.noncritical e -> raise (Faulty f)
end
@@ -452,13 +452,13 @@ let intern_from_file f =
module DPMap = Map.Make(DirPath)
let rec intern_library (needed, contents) (dir, f) from =
- Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* Look if in the current logical environment *)
try (find_library dir).libsum_digests, (needed, contents)
with Not_found ->
(* Look if already listed and consequently its dependencies too *)
try (DPMap.find dir contents).library_digests, (needed, contents)
with Not_found ->
+ Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
(* [dir] is an absolute name which matches [f] which must be in loadpath *)
let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
let m = intern_from_file f in
@@ -468,16 +468,18 @@ let rec intern_library (needed, contents) (dir, f) from =
pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
spc() ++ pr_dirpath dir);
Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
- m.library_digests, intern_library_deps (needed, contents) dir m (Some f)
+ m.library_digests, intern_library_deps (needed, contents) dir m f
and intern_library_deps libs dir m from =
let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in
(dir :: needed, DPMap.add dir m contents )
and intern_mandatory_library caller from libs (dir,d) =
- let digest, libs = intern_library libs (dir, None) from in
+ let digest, libs = intern_library libs (dir, None) (Some from) in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
- errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir);
+ errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++
+ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
+ over library " ++ pr_dirpath dir);
libs
let rec_intern_library libs (dir, f) =
@@ -551,12 +553,20 @@ let in_require : require_obj -> obj =
let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
+let warn_require_in_module =
+ CWarnings.create ~name:"require-in-module" ~category:"deprecated"
+ (fun () -> strbrk "Require inside a module is" ++
+ strbrk " deprecated and strongly discouraged. " ++
+ strbrk "You can Require a module at toplevel " ++
+ strbrk "and optionally Import it inside another one.")
+
let require_library_from_dirpath modrefl export =
let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in
let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
let modrefl = List.map fst modrefl in
if Lib.is_module_or_modtype () then
begin
+ warn_require_in_module ();
add_anonymous_leaf (in_require (needed,modrefl,None));
Option.iter (fun exp ->
add_anonymous_leaf (in_import_library (modrefl,exp)))
@@ -724,7 +734,7 @@ let save_library_to ?todo dir f otab =
except Int.Set.empty in
let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
Array.iteri (fun i x ->
- if not(is_done_or_todo i x) then Errors.errorlabstrm "library"
+ if not(is_done_or_todo i x) then CErrors.errorlabstrm "library"
Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
opaque_table;
let sd = {
@@ -756,8 +766,8 @@ let save_library_to ?todo dir f otab =
if not (Nativelib.compile_library dir ast fn) then
error "Could not compile the library to native code."
with reraise ->
- let reraise = Errors.push reraise in
- let () = Feedback.msg_notice (str "Removed file " ++ str f') in
+ let reraise = CErrors.push reraise in
+ let () = Feedback.msg_warning (str "Removed file " ++ str f') in
let () = close_out ch in
let () = Sys.remove f' in
iraise reraise
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 6f4d79430d..d03c6c5553 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -8,7 +8,7 @@
open Pp
open Util
-open Errors
+open CErrors
open Names
open Libnames
@@ -72,9 +72,6 @@ let add_load_path phys_path coq_path ~implicit =
let replace =
if DirPath.equal coq_path old_path then
implicit <> old_implicit
- else if DirPath.equal coq_path (Nameops.default_root_prefix)
- && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
- false (* This is the default "-I ." path, don't override the old path *)
else
let () =
(* Do not warn when overriding the default "-I ." path *)
diff --git a/library/nametab.ml b/library/nametab.ml
index f533bc7914..fa5db37ed5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/library/states.ml b/library/states.ml
index 2e1be764ab..95bd819d66 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -35,7 +35,7 @@ let with_state_protection f x =
try
let a = f x in unfreeze st; a
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
(unfreeze st; iraise reraise)
let with_state_protection_on_exception = Future.transactify
diff --git a/library/summary.ml b/library/summary.ml
index edea7dbe50..6efa07f388 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
module Dyn = Dyn.Make(struct end)
@@ -105,10 +105,10 @@ let unfreeze_summaries fs =
in
let fold id decl state =
try fold id decl state
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
- (name_of_summary id) (Pp.string_of_ppcmds (Errors.iprint e));
+ (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
iraise e
in
(** We rely on the order of the frozen list, and the order of folding *)
@@ -149,7 +149,7 @@ let unfreeze_summary datas =
let (name, summary) = Int.Map.find id !summaries in
try summary.unfreeze_function data
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
prerr_endline ("Exception unfreezing " ^ name);
iraise e)
datas
@@ -186,4 +186,29 @@ let ref ?(freeze=fun _ r -> r) ~name x =
init_function = (fun () -> r := x) };
r
+module Local = struct
+
+type 'a local_ref = ('a CEphemeron.key * string) ref
+
+let (:=) r v = r := (CEphemeron.create v, snd !r)
+
+let (!) r =
+ let key, name = !r in
+ try CEphemeron.get key
+ with CEphemeron.InvalidKey ->
+ let _, { init_function } =
+ Int.Map.find (String.hash (mangle name)) !summaries in
+ init_function ();
+ CEphemeron.get (fst !r)
+
+let ref ?(freeze=fun x -> x) ~name init =
+ let r = Pervasives.ref (CEphemeron.create init, name) in
+ declare_summary name
+ { freeze_function = (fun _ -> freeze !r);
+ unfreeze_function = ((:=) r);
+ init_function = (fun () -> r := init) };
+ r
+
+end
+
let dump = Dyn.dump
diff --git a/library/summary.mli b/library/summary.mli
index 27889cab27..1b57613cb7 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -42,6 +42,17 @@ val declare_summary : string -> 'a summary_declaration -> unit
val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
+(* As [ref] but the value is local to a process, i.e. not sent to, say, proof
+ * workers. It is useful to implement a local cache for example. *)
+module Local : sig
+
+ type 'a local_ref
+ val ref : ?freeze:('a -> 'a) -> name:string -> 'a -> 'a local_ref
+ val (:=) : 'a local_ref -> 'a -> unit
+ val (!) : 'a local_ref -> 'a
+
+end
+
(** Special name for the summary of ML modules. This summary entry is
special because its unfreeze may load ML code and hence add summary
entries. Thus is has to be recognizable, and handled appropriately *)
diff --git a/library/universes.ml b/library/universes.ml
index 21d960ea36..db95607f18 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -112,7 +112,7 @@ let enforce_eq_instances_univs strict x y c =
let d = if strict then ULub else UEq in
let ax = Instance.to_array x and ay = Instance.to_array y in
if Array.length ax != Array.length ay then
- Errors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
+ CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
Pp.str " instances of different lengths");
CArray.fold_right2
(fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
@@ -337,7 +337,7 @@ let existing_instance ctx inst =
and a2 = Instance.to_array (UContext.instance ctx) in
let len1 = Array.length a1 and len2 = Array.length a2 in
if not (len1 == len2) then
- Errors.errorlabstrm "Universes"
+ CErrors.errorlabstrm "Universes"
(str "Polymorphic constant expected " ++ int len2 ++
str" levels but was given " ++ int len1)
else ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 18:39:19 +0000