aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml4
-rw-r--r--vernac/attributes.mli3
-rw-r--r--vernac/canonical.ml8
-rw-r--r--vernac/classes.ml9
-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/declareUniv.ml2
-rw-r--r--vernac/egramcoq.ml4
-rw-r--r--vernac/egramcoq.mli3
-rw-r--r--vernac/g_vernac.mlg5
-rw-r--r--vernac/himsg.ml6
-rw-r--r--vernac/library.ml66
-rw-r--r--vernac/loadpath.ml40
-rw-r--r--vernac/metasyntax.ml15
-rw-r--r--vernac/mltop.ml64
-rw-r--r--vernac/mltop.mli7
-rw-r--r--vernac/ppvernac.ml4
-rw-r--r--vernac/prettyp.ml22
-rw-r--r--vernac/prettyp.mli4
-rw-r--r--vernac/record.ml6
-rw-r--r--vernac/topfmt.ml4
-rw-r--r--vernac/vernac.mllib2
-rw-r--r--vernac/vernacentries.ml45
-rw-r--r--vernac/vernacexpr.ml2
26 files changed, 172 insertions, 165 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index b7a3b002bd..68d2c3a00d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -234,5 +234,7 @@ let only_polymorphism atts = parse polymorphic atts
let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
-let canonical =
+let canonical_field =
enable_attribute ~key:"canonical" ~default:(fun () -> true)
+let canonical_instance =
+ enable_attribute ~key:"canonical" ~default:(fun () -> false)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 34ff15ca7d..0074db66d3 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -48,7 +48,8 @@ val program : bool attribute
val template : bool option attribute
val locality : bool option attribute
val deprecation : Deprecation.t option attribute
-val canonical : bool attribute
+val canonical_field : bool attribute
+val canonical_instance : bool attribute
val program_mode_option_name : string list
(** For internal use when messing with the global option. *)
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index 141b02ef63..e41610b532 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -21,10 +21,12 @@ let cache_canonical_structure (_, (o,_)) =
let sigma = Evd.from_env env in
register_canonical_structure ~warn:true env sigma o
-let discharge_canonical_structure (_,(x, local)) =
- if local then None else Some (x, local)
+let discharge_canonical_structure (_,((gref, _ as x), local)) =
+ if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None
+ else Some (x, local)
-let inCanonStruc : (Constant.t * inductive) * bool -> obj =
+
+let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
declare_object {(default_object "CANONICAL-STRUCTURE") with
open_function = open_canonical_structure;
cache_function = cache_canonical_structure;
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c9b5144299..77bc4e4f8a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -42,13 +42,10 @@ let () =
Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
let add_instance_hint inst path local info poly =
- let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
- | IsGlobal gr -> Hints.IsGlobRef gr
- in
Flags.silently (fun () ->
Hints.add_hints ~local [typeclasses_db]
(Hints.HintsResolveEntry
- [info, poly, false, Hints.PathHints path, inst'])) ()
+ [info, poly, false, Hints.PathHints path, inst])) ()
let is_local_for_hint i =
match i.is_global with
@@ -61,9 +58,9 @@ let is_local_for_hint i =
let add_instance check inst =
let poly = Global.is_polymorphic inst.is_impl in
let local = is_local_for_hint inst in
- add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local
+ add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local
inst.is_info poly;
- List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
+ List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path
local pri poly)
(build_subclasses ~check:(check && not (isVarRef inst.is_impl))
(Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
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/declareUniv.ml b/vernac/declareUniv.ml
index 69ba9d76ec..def2fdad2a 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -72,7 +72,7 @@ let declare_univ_binders gr pl =
CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
| ConstructRef _ ->
CErrors.anomaly ~label:"declare_univ_binders"
- Pp.(str "declare_univ_binders on an constructor reference")
+ Pp.(str "declare_univ_binders on a constructor reference")
in
let univs = Id.Map.fold (fun id univ univs ->
match Univ.Level.name univ with
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index b65a126f55..07656f9715 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -278,6 +278,10 @@ let find_custom_entry s =
try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
+let exists_custom_entry s = match find_custom_entry s with
+| _ -> true
+| exception _ -> false
+
let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality
(* This computes the name of the level where to add a new rule *)
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index f879d51660..6768d24d5c 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -19,4 +19,7 @@ val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
(** Add a term notation rule to the parsing system. *)
val create_custom_entry : local:bool -> string -> unit
+
+val exists_custom_entry : string -> bool
+
val locality_of_custom_entry : string -> bool
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 436648c163..3302231fd1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -471,7 +471,7 @@ GRAMMAR EXTEND Gram
[ [ attr = LIST0 quoted_attributes ;
bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
rf_notation = decl_notation -> {
- let rf_canonical = attr |> List.flatten |> parse canonical in
+ let rf_canonical = attr |> List.flatten |> parse canonical_field in
let rf_subclass, rf_decl = bd in
rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
;
@@ -1026,7 +1026,8 @@ GRAMMAR EXTEND Gram
| IDENT "Coercions" -> { PrintCoercions }
| IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
-> { PrintCoercionPaths (s,t) }
- | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions }
+ | IDENT "Canonical"; IDENT "Projections"; qids = LIST0 smart_global
+ -> { PrintCanonicalConversions qids }
| IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags }
| IDENT "Tables" -> { PrintTables }
| IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) }
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 19ec0a3642..eb39564fed 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -297,6 +297,7 @@ let explain_unification_error env sigma p1 p2 = function
strbrk " with term " ++ pr_leconstr_env env sigma rhs ++
strbrk " that would depend on itself"]
| NotClean ((evk,args),env,c) ->
+ let env = make_all_name_different env sigma in
[str "cannot instantiate " ++ quote (pr_existential_key sigma evk)
++ strbrk " because " ++ pr_leconstr_env env sigma c ++
strbrk " is not in its scope" ++
@@ -605,7 +606,7 @@ let rec explain_evar_kind env sigma evk ty =
let explain_typeclass_resolution env sigma evi k =
match Typeclasses.class_of_constr env sigma evi.evar_concl with
| Some _ ->
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
fnl () ++ str "Could not find an instance for " ++
pr_leconstr_env env sigma evi.evar_concl ++
pr_trailing_ne_context_of env sigma
@@ -622,7 +623,7 @@ let explain_placeholder_kind env sigma c e =
let explain_unsolvable_implicit env sigma evk explain =
let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in
let pe = pr_trailing_ne_context_of env sigma in
strbrk "Cannot infer " ++
@@ -1363,7 +1364,6 @@ let explain_exn_default = function
| Sys_error msg -> hov 0 (str "System error: " ++ quote (str msg))
| Out_of_memory -> hov 0 (str "Out of memory.")
| Stack_overflow -> hov 0 (str "Stack overflow.")
- | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
| CErrors.Timeout -> hov 0 (str "Timeout!")
| Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
(* Otherwise, not handled here *)
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/loadpath.ml b/vernac/loadpath.ml
index a8462e31e1..506b3bc505 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -138,27 +138,31 @@ let select_vo_file ~warn loadpath base =
System.where_in_path ~warn loadpath name in
Some (lpath, file)
with Not_found -> None in
+ (* If [!Flags.load_vos_libraries]
+ and the .vos file exists
+ and this file is not empty
+ Then load this library
+ Else load the most recent between the .vo file and the .vio file,
+ or if there is only of the two files, take this one,
+ or raise an error if both are missing. *)
+ let load_most_recent_of_vo_and_vio () =
+ match find ".vo", find ".vio" with
+ | None, None ->
+ Error LibNotFound
+ | Some res, None | None, Some res ->
+ Ok res
+ | Some (_, vo), Some (_, vi as resvi)
+ when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
+ warn_several_object_files (vi, vo);
+ Ok resvi
+ | Some resvo, Some _ ->
+ Ok resvo
+ in
if !Flags.load_vos_libraries then begin
- (* If the .vos file exists and is not empty, it describes the library.
- Otherwise, load the .vo file, or fail if is missing. *)
match find ".vos" with
| Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos
- | _ ->
- match find ".vo" with
- | None -> Error LibNotFound
- | Some resvo -> Ok resvo
- end else
- match find ".vo", find ".vio" with
- | None, None ->
- Error LibNotFound
- | Some res, None | None, Some res ->
- Ok res
- | Some (_, vo), Some (_, vi as resvi)
- when Unix.((stat vo).st_mtime < (stat vi).st_mtime) ->
- warn_several_object_files (vi, vo);
- Ok resvi
- | Some resvo, Some _ ->
- Ok resvo
+ | _ -> load_most_recent_of_vo_and_vio()
+ end else load_most_recent_of_vo_and_vio()
let locate_absolute_library dir : CUnix.physical_path locate_result =
(* Search in loadpath *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 35681aed13..05e23164b1 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1346,7 +1346,7 @@ let inNotation : notation_obj -> obj =
(**********************************************************************)
let with_lib_stk_protection f x =
- let fs = Lib.freeze ~marshallable:false in
+ let fs = Lib.freeze () in
try let a = f x in Lib.unfreeze fs; a
with reraise ->
let reraise = CErrors.push reraise in
@@ -1654,10 +1654,16 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
(**********************************************************************)
(* Declaration of custom entry *)
+let warn_custom_entry =
+ CWarnings.create ~name:"custom-entry-overriden" ~category:"parsing"
+ (fun s ->
+ strbrk "Custom entry " ++ str s ++ strbrk " has been overriden.")
+
let load_custom_entry _ _ = ()
let open_custom_entry _ (_,(local,s)) =
- Egramcoq.create_custom_entry ~local s
+ if Egramcoq.exists_custom_entry s then warn_custom_entry s
+ else Egramcoq.create_custom_entry ~local s
let cache_custom_entry o =
load_custom_entry 1 o;
@@ -1677,4 +1683,7 @@ let inCustomEntry : locality_flag * string -> obj =
classify_function = classify_custom_entry}
let declare_custom_entry local s =
- Lib.add_anonymous_leaf (inCustomEntry (local,s))
+ if Egramcoq.exists_custom_entry s then
+ user_err Pp.(str "Custom entry " ++ str s ++ str " already exists")
+ else
+ Lib.add_anonymous_leaf (inCustomEntry (local,s))
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 9c18441d9c..2bac35b08f 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -56,7 +56,6 @@ let keep_copy_mlpath path =
(* If there is a toplevel under Coq *)
type toplevel = {
load_obj : string -> unit;
- use_file : string -> unit;
add_dir : string -> unit;
ml_loop : unit -> unit }
@@ -94,43 +93,26 @@ let ocaml_toploop () =
| WithTop t -> Printexc.catch t.ml_loop ()
| _ -> ()
-(* Try to interpret load_obj's (internal) errors *)
-let report_on_load_obj_error exc =
- let x = Obj.repr exc in
- (* Try an horrible (fragile) hack to report on Symtable dynlink errors *)
- (* (we follow ocaml's Printexc.to_string decoding of exceptions) *)
- if Obj.is_block x && String.equal (Obj.magic (Obj.field (Obj.field x 0) 0)) "Symtable.Error"
- then
- let err_block = Obj.field x 1 in
- if Int.equal (Obj.tag err_block) 0 then
- (* Symtable.Undefined_global of string *)
- str "reference to undefined global " ++
- str (Obj.magic (Obj.field err_block 0))
- else str (Printexc.to_string exc)
- else str (Printexc.to_string exc)
-
(* Dynamic loading of .cmo/.cma *)
+(* We register errors at least for Dynlink, it is possible to do so Symtable
+ too, as we do in the bytecode init code.
+*)
+let _ = CErrors.register_handler (function
+ | Dynlink.Error e ->
+ hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
+ | _ ->
+ raise CErrors.Unhandled
+ )
+
let ml_load s =
- match !load with
- | WithTop t ->
- (try t.load_obj s; s
- with
- | e when CErrors.noncritical e ->
- let e = CErrors.push e in
- match fst e with
- | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e)
- | exc ->
- let msg = report_on_load_obj_error exc in
- user_err ~hdr:"Mltop.load_object" (str"Cannot link ml-object " ++
- str s ++ str" to Coq code (" ++ msg ++ str ")."))
- | WithoutTop ->
- try
- Dynlink.loadfile s; s
- with Dynlink.Error a ->
- user_err ~hdr:"Mltop.load_object"
- (strbrk "while loading " ++ str s ++
- strbrk ": " ++ str (Dynlink.error_message a))
+ (match !load with
+ | WithTop t ->
+ t.load_obj s
+ | WithoutTop ->
+ Dynlink.loadfile s
+ );
+ s
let dir_ml_load s =
match !load with
@@ -140,17 +122,6 @@ let dir_ml_load s =
let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
ml_load gname
-(* Dynamic interpretation of .ml *)
-let dir_ml_use s =
- match !load with
- | WithTop t -> t.use_file s
- | _ ->
- let moreinfo =
- if Sys.(backend_type = Native) then " Loading ML code works only in bytecode."
- else ""
- in
- user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
-
(* Adds a path to the ML paths *)
let add_ml_dir s =
match !load with
@@ -275,7 +246,6 @@ let load_ml_object mname ?path fname=
init_ml_object mname;
path
-let dir_ml_load m = ignore(dir_ml_load m)
let add_known_module m = add_known_module m None
(* Summary of declared ML Modules *)
diff --git a/vernac/mltop.mli b/vernac/mltop.mli
index 56a28b64b0..271772d7ba 100644
--- a/vernac/mltop.mli
+++ b/vernac/mltop.mli
@@ -14,7 +14,6 @@
record. *)
type toplevel = {
load_obj : string -> unit;
- use_file : string -> unit;
add_dir : string -> unit;
ml_loop : unit -> unit }
@@ -38,12 +37,6 @@ val add_ml_dir : recursive:bool -> string -> unit
(** Tests if we can load ML files *)
val has_dynlink : bool
-(** Dynamic loading of .cmo *)
-val dir_ml_load : string -> unit
-
-(** Dynamic interpretation of .ml *)
-val dir_ml_use : string -> unit
-
(** List of modules linked to the toplevel *)
val add_known_module : string -> unit
val module_is_known : string -> bool
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1742027076..a1bd99c237 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -513,8 +513,8 @@ let string_of_theorem_kind = let open Decls in function
keyword "Print Coercion Paths" ++ spc()
++ pr_class_rawexpr s ++ spc()
++ pr_class_rawexpr t
- | PrintCanonicalConversions ->
- keyword "Print Canonical Structures"
+ | PrintCanonicalConversions qids ->
+ keyword "Print Canonical Structures" ++ prlist pr_smart_global qids
| PrintTypingFlags ->
keyword "Print Typing Flags"
| PrintTables ->
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ec8658d939..2cd1cf7c65 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 []
(*******************)
(* *)
@@ -972,7 +972,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
@@ -986,7 +986,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())
@@ -1017,12 +1017,24 @@ let print_path_between cls clt =
in
print_path ((i,j),p)
-let print_canonical_projections env sigma =
+let print_canonical_projections env sigma grefs =
+ let match_proj_gref ((x,y),c) gr =
+ GlobRef.equal x gr ||
+ begin match y with
+ | Const_cs y -> GlobRef.equal y gr
+ | _ -> false
+ end ||
+ GlobRef.equal c.o_ORIGIN gr
+ in
+ let projs =
+ List.filter (fun p -> List.for_all (match_proj_gref p) grefs)
+ (canonical_projections ())
+ in
prlist_with_sep fnl
(fun ((r1,r2),o) -> pr_cs_pattern r2 ++
str " <- " ++
pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
- (canonical_projections ())
+ projs
(*************************************************************************)
diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli
index dc4280f286..ac41f30c5d 100644
--- a/vernac/prettyp.mli
+++ b/vernac/prettyp.mli
@@ -52,8 +52,8 @@ 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_canonical_projections : env -> Evd.evar_map -> Pp.t
+val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
+val print_canonical_projections : env -> Evd.evar_map -> GlobRef.t list -> Pp.t
(** Pretty-printing functions for type classes and instances *)
val print_typeclasses : unit -> Pp.t
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/topfmt.ml b/vernac/topfmt.ml
index 45f40b1258..de02f7ecfb 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -359,7 +359,7 @@ let in_phase ~phase f x =
default_phase := op;
res
with exn ->
- let iexn = Backtrace.add_backtrace exn in
+ let iexn = Exninfo.capture exn in
default_phase := op;
Util.iraise iexn
@@ -415,7 +415,7 @@ let with_output_to_file fname func input =
close_out channel;
output
with reraise ->
- let reraise = Backtrace.add_backtrace reraise in
+ let reraise = Exninfo.capture reraise in
std_ft := Util.pi1 old_fmt;
err_ft := Util.pi2 old_fmt;
deep_ft := Util.pi3 old_fmt;
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 833c279320..6e398d87ca 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -20,7 +20,7 @@ Canonical
RecLemmas
Library
Lemmas
-Class
+ComCoercion
Auto_ind_decl
Indschemes
Obligations
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 439ec61d38..d011fb2e77 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)
@@ -63,14 +63,15 @@ module DefAttributes = struct
polymorphic : bool;
program : bool;
deprecated : Deprecation.t option;
+ canonical_instance : bool;
}
let parse f =
let open Attributes in
- let ((locality, deprecated), polymorphic), program =
- parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f
+ let (((locality, deprecated), polymorphic), program), canonical_instance =
+ parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f
in
- { polymorphic; program; locality; deprecated }
+ { polymorphic; program; locality; deprecated; canonical_instance }
end
let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -474,7 +475,7 @@ let program_inference_hook env sigma ev =
let tac = !Obligations.default_tactic in
let evi = Evd.find sigma ev in
let evi = Evarutil.nf_evar_info sigma evi in
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
try
let concl = evi.Evd.evar_concl in
if not (Evarutil.is_ground_env sigma env &&
@@ -522,13 +523,17 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
in
start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
-let vernac_definition_hook ~local ~poly = let open Decls in function
+let vernac_definition_hook ~canonical_instance ~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)
+| Definition when canonical_instance ->
+ Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
+| Let when canonical_instance ->
+ Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
| _ -> None
let fresh_name_for_anonymous_theorem () =
@@ -551,7 +556,7 @@ let vernac_definition_name lid local =
let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
- let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in
+ let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
let program_mode = atts.program in
let poly = atts.polymorphic in
let name = vernac_definition_name lid local in
@@ -560,7 +565,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
let scope = enforce_locality_exp atts.locality discharge in
- let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in
+ let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
let program_mode = atts.program in
let name = vernac_definition_name lid scope in
let red_option = match red_option with
@@ -1034,7 +1039,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 +1047,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 *)
@@ -1448,6 +1453,14 @@ let () =
optread = Nativenorm.get_profiling_enabled;
optwrite = Nativenorm.set_profiling_enabled }
+let () =
+ declare_bool_option
+ { optdepr = false;
+ optname = "enable native compute timing";
+ optkey = ["NativeCompute"; "Timing"];
+ optread = Nativenorm.get_timing_enabled;
+ optwrite = Nativenorm.set_timing_enabled }
+
let _ =
declare_bool_option
{ optdepr = false;
@@ -1701,7 +1714,9 @@ let vernac_print ~pstate ~atts =
| PrintCoercions -> Prettyp.print_coercions ()
| PrintCoercionPaths (cls,clt) ->
Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
- | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
+ | PrintCanonicalConversions qids ->
+ let grefs = List.map Smartlocate.smart_global qids in
+ Prettyp.print_canonical_projections env sigma grefs
| PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst
| PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
| PrintHintGoal ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 32ff8b8fb2..1daa244986 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -46,7 +46,7 @@ type printable =
| PrintInstances of qualid or_by_notation
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
- | PrintCanonicalConversions
+ | PrintCanonicalConversions of qualid or_by_notation list
| PrintUniverses of bool * qualid list option * string option
| PrintHint of qualid or_by_notation
| PrintHintGoal
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:17:19 +0000