aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/comAssumption.ml4
-rw-r--r--vernac/comCoercion.ml (renamed from vernac/class.ml)4
-rw-r--r--vernac/comCoercion.mli (renamed from vernac/class.mli)2
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/library.ml66
-rw-r--r--vernac/prettyp.ml6
-rw-r--r--vernac/prettyp.mli2
-rw-r--r--vernac/record.ml6
-rw-r--r--vernac/vernac.mllib2
-rw-r--r--vernac/vernacentries.ml14
10 files changed, 51 insertions, 57 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 8a403e5a03..625ffb5a06 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
let env = Global.env () in
let sigma = Evd.from_env env in
let () = Classes.declare_instance env sigma None true r in
- let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
+ let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false in
()
let instance_of_univ_entry = function
@@ -65,7 +65,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name
| Declare.ImportNeedQualified -> true
| Declare.ImportDefaultBehavior -> false
in
- let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
+ let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in
let inst = instance_of_univ_entry univs in
(gr,inst)
diff --git a/vernac/class.ml b/vernac/comCoercion.ml
index 3c43b125d1..56ab6f289d 100644
--- a/vernac/class.ml
+++ b/vernac/comCoercion.ml
@@ -18,7 +18,7 @@ open Context
open Vars
open Termops
open Environ
-open Classops
+open Coercionops
open Declare
open Libobject
@@ -231,7 +231,7 @@ let check_source = function
let cache_coercion (_,c) =
let env = Global.env () in
let sigma = Evd.from_env env in
- Classops.declare_coercion env sigma c
+ Coercionops.declare_coercion env sigma c
let open_coercion i o =
if Int.equal i 1 then
diff --git a/vernac/class.mli b/vernac/comCoercion.mli
index 3254d5d981..f98ef4fdd6 100644
--- a/vernac/class.mli
+++ b/vernac/comCoercion.mli
@@ -9,7 +9,7 @@
(************************************************************************)
open Names
-open Classops
+open Coercionops
(** Classes and coercions. *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index b603c54026..8de1c69424 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -553,7 +553,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
(* Declare the possible notations of inductive types *)
List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
(* Declare the coercions *)
- List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
+ List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
diff --git a/vernac/library.ml b/vernac/library.ml
index 244424de6b..0f7e7d2aa0 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -430,6 +430,22 @@ let error_recursively_dependent_library dir =
(* Security weakness: file might have been changed on disk between
writing the content and computing the checksum... *)
+let save_library_base f sum lib univs tasks proofs =
+ let ch = raw_extern_library f in
+ try
+ System.marshal_out_segment f ch (sum : seg_sum);
+ System.marshal_out_segment f ch (lib : seg_lib);
+ System.marshal_out_segment f ch (univs : seg_univ option);
+ System.marshal_out_segment f ch (tasks : 'tasks option);
+ System.marshal_out_segment f ch (proofs : seg_proofs);
+ close_out ch
+ with reraise ->
+ let reraise = CErrors.push reraise in
+ close_out ch;
+ Feedback.msg_warning (str "Removed file " ++ str f);
+ Sys.remove f;
+ iraise reraise
+
type ('document,'counters) todo_proofs =
| ProofsTodoNone (* for .vo *)
| ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *)
@@ -454,18 +470,17 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
match todo_proofs with
| ProofsTodoNone -> None, None
| ProofsTodoSomeEmpty _except ->
- None,
- Some (Univ.ContextSet.empty,false)
+ None, Some (Univ.ContextSet.empty,false)
| ProofsTodoSome (_except, tasks, rcbackup) ->
- let tasks =
- List.map Stateid.(fun (r,b) ->
+ let tasks =
+ List.map Stateid.(fun (r,b) ->
try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b
with Not_found -> assert b; { r with uuid = -1 }, b)
tasks in
- Some (tasks,rcbackup),
- Some (Univ.ContextSet.empty,false)
- in
- let sd = {
+ Some (tasks,rcbackup),
+ Some (Univ.ContextSet.empty,false)
+ in
+ let sd = {
md_name = dir;
md_deps = Array.of_list (current_deps ());
} in
@@ -475,36 +490,15 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
} in
if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
error_recursively_dependent_library dir;
- (* Open the vo file and write the magic number *)
- let f' = f in
- let ch = raw_extern_library f' in
- try
- (* Writing vo payload *)
- System.marshal_out_segment f' ch (sd : seg_sum);
- System.marshal_out_segment f' ch (md : seg_lib);
- System.marshal_out_segment f' ch (utab : seg_univ option);
- System.marshal_out_segment f' ch (tasks : 'tasks option);
- System.marshal_out_segment f' ch (opaque_table : seg_proofs);
- close_out ch;
- (* Writing native code files *)
- if output_native_objects then
- let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
- Nativelib.compile_library dir ast fn
- with reraise ->
- 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
+ (* Writing vo payload *)
+ save_library_base f sd md utab tasks opaque_table;
+ (* Writing native code files *)
+ if output_native_objects then
+ let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in
+ Nativelib.compile_library dir ast fn
let save_library_raw f sum lib univs proofs =
- let ch = raw_extern_library f in
- System.marshal_out_segment f ch (sum : seg_sum);
- System.marshal_out_segment f ch (lib : seg_lib);
- System.marshal_out_segment f ch (Some univs : seg_univ option);
- System.marshal_out_segment f ch (None : 'tasks option);
- System.marshal_out_segment f ch (proofs : seg_proofs);
- close_out ch
+ save_library_base f sum lib (Some univs) None proofs
module StringOrd = struct type t = string let compare = String.compare end
module StringSet = Set.Make(StringOrd)
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index eb7b28f15b..d04a02febc 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -199,7 +199,7 @@ let print_opacity ref =
(*******************)
let print_if_is_coercion ref =
- if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+ if Coercionops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
(*******************)
(* *)
@@ -951,7 +951,7 @@ let inspect env sigma depth =
(*************************************************************************)
(* Pretty-printing functions coming from classops.ml *)
-open Classops
+open Coercionops
let print_coercion_value v = Printer.pr_global v.coe_value
@@ -965,7 +965,7 @@ let print_path ((i,j),p) =
str"] : ") ++
print_class i ++ str" >-> " ++ print_class j
-let _ = Classops.install_path_printer print_path
+let _ = Coercionops.install_path_printer print_path
let print_graph () =
prlist_with_sep fnl print_path (inheritance_graph())
diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli
index dc4280f286..2ee9c4ed33 100644
--- a/vernac/prettyp.mli
+++ b/vernac/prettyp.mli
@@ -52,7 +52,7 @@ val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
val print_graph : unit -> Pp.t
val print_classes : unit -> Pp.t
val print_coercions : unit -> Pp.t
-val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
+val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
val print_canonical_projections : env -> Evd.evar_map -> Pp.t
(** Pretty-printing functions for type classes and instances *)
diff --git a/vernac/record.ml b/vernac/record.ml
index ea10e06d02..df9b4a0914 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -366,8 +366,8 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
let refi = GlobRef.ConstRef kn in
Impargs.maybe_declare_manual_implicits false refi impls;
if flags.pf_subclass then begin
- let cl = Class.class_of_global (GlobRef.IndRef indsp) in
- Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
+ let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
+ ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
end;
let i = if is_local_assum decl then i+1 else i in
(Some kn::sp_projs, i, Projection term::subst)
@@ -489,7 +489,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let cstr = (rsp, 1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
let build = GlobRef.ConstructRef cstr in
- let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in
+ let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in
let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
rsp
in
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 5226c2ba65..7b4924eaed 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -21,7 +21,7 @@ RecLemmas
Library
Prettyp
Lemmas
-Class
+ComCoercion
Auto_ind_decl
Search
Indschemes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 439ec61d38..604d1b28ff 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -49,9 +49,9 @@ let get_goal_or_global_context ~pstate glnum =
| Some p -> Pfedit.get_goal_context p glnum
let cl_of_qualid = function
- | FunClass -> Classops.CL_FUN
- | SortClass -> Classops.CL_SORT
- | RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r)
+ | FunClass -> Coercionops.CL_FUN
+ | SortClass -> Coercionops.CL_SORT
+ | RefClass r -> ComCoercion.class_of_global (Smartlocate.smart_global ~head:true r)
let scope_class_of_qualid qid =
Notation.scope_class_of_class (cl_of_qualid qid)
@@ -524,11 +524,11 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
let vernac_definition_hook ~local ~poly = let open Decls in function
| Coercion ->
- Some (Class.add_coercion_hook ~poly)
+ Some (ComCoercion.add_coercion_hook ~poly)
| CanonicalStructure ->
Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
| SubClass ->
- Some (Class.add_subclass_hook ~poly)
+ Some (ComCoercion.add_subclass_hook ~poly)
| _ -> None
let fresh_name_for_anonymous_theorem () =
@@ -1034,7 +1034,7 @@ let vernac_coercion ~atts ref qids qidt =
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
let ref' = smart_global ref in
- Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
+ ComCoercion.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
let vernac_identity_coercion ~atts id qids qidt =
@@ -1042,7 +1042,7 @@ let vernac_identity_coercion ~atts id qids qidt =
let local = enforce_locality local in
let target = cl_of_qualid qidt in
let source = cl_of_qualid qids in
- Class.try_add_new_identity_coercion id ~local ~poly ~source ~target
+ ComCoercion.try_add_new_identity_coercion id ~local ~poly ~source ~target
(* Type classes *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:10:17 +0000