aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.make3
-rw-r--r--coq.opam2
-rw-r--r--engine/proofview.ml18
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--plugins/extraction/extract_env.ml37
-rw-r--r--proofs/proof.ml15
-rw-r--r--proofs/proof_bullet.ml7
-rw-r--r--tactics/pfedit.ml2
-rw-r--r--vernac/vernacstate.ml2
10 files changed, 27 insertions, 63 deletions
diff --git a/Makefile.make b/Makefile.make
index e19053462d..e63a578e37 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -56,6 +56,7 @@ FIND_SKIP_DIRS:=-not -name . '(' \
-name "$${GIT_DIR}" -o \
-name '_build' -o \
-name '_build_ci' -o \
+ -name '_build_boot' -o \
-name '_install_ci' -o \
-name 'gramlib' -o \
-name 'user-contrib' -o \
@@ -251,7 +252,7 @@ docclean:
rm -rf doc/sphinx/_build
archclean: clean-ide optclean voclean plugin-tutorialclean
- rm -rf _build
+ rm -rf _build _build_boot
rm -f $(ALLSTDLIB).*
optclean:
diff --git a/coq.opam b/coq.opam
index 50f746abec..39191c21d9 100644
--- a/coq.opam
+++ b/coq.opam
@@ -28,7 +28,7 @@ depends: [
]
build: [
- [ "./configure" "-prefix" prefix "-native-compiler" "no" ]
+ [ "./configure" "-prefix" prefix ]
[ "make" "-f" "Makefile.dune" "voboot" ]
[ "dune" "build" "-p" name "-j" jobs ]
]
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 16be96454e..b0ea75ac60 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -302,7 +302,8 @@ let tclONCE = Proof.once
exception MoreThanOneSuccess
let _ = CErrors.register_handler begin function
- | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.")
+ | MoreThanOneSuccess ->
+ Pp.str "This tactic has more than one success."
| _ -> raise CErrors.Unhandled
end
@@ -347,8 +348,7 @@ exception NoSuchGoals of int
let _ = CErrors.register_handler begin function
| NoSuchGoals n ->
- CErrors.user_err
- (str "No such " ++ str (String.plural n "goal") ++ str ".")
+ str "No such " ++ str (String.plural n "goal") ++ str "."
| _ -> raise CErrors.Unhandled
end
@@ -420,12 +420,9 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
exception SizeMismatch of int*int
let _ = CErrors.register_handler begin function
| SizeMismatch (i,j) ->
- let open Pp in
- let errmsg =
- str"Incorrect number of goals" ++ spc() ++
- str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
- in
- CErrors.user_err errmsg
+ let open Pp in
+ str"Incorrect number of goals" ++ spc() ++
+ str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
| _ -> raise CErrors.Unhandled
end
@@ -910,7 +907,8 @@ let tclPROGRESS t =
tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
let _ = CErrors.register_handler begin function
- | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+ | Logic_monad.Tac_Timeout ->
+ Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!"
| _ -> raise CErrors.Unhandled
end
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f6f2058c13..e8adde2605 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -321,6 +321,8 @@ let universes_of_private eff =
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
+let structure_body_of_safe_env env = env.revstruct
+
let sections_of_safe_env senv = senv.sections
let get_section = function
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 92bbd264fa..e6f2fc4a5d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -37,6 +37,8 @@ val env_of_safe_env : safe_environment -> Environ.env
val sections_of_safe_env : safe_environment -> section_data Section.t option
+val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
+
(** The safe_environment state monad *)
type safe_transformer0 = safe_environment -> safe_environment
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2dc3e8a934..853be82eb8 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -26,43 +26,8 @@ open Common
(*S Part I: computing Coq environment. *)
(***************************************)
-(* FIXME: this is a Libobject hack that should be removed. *)
-module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> (Label.t * structure_field_body) option end)
-
-let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
-| f -> f o
-| exception Not_found -> None
-
let toplevel_env () =
- let get_reference = function
- | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
- let mp,l = KerName.repr kn in
- let handler =
- DynHandle.add Declare.Internal.objConstant begin fun _ ->
- let constant = Global.lookup_constant (Constant.make1 kn) in
- Some (l, SFBconst constant)
- end @@
- DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
- let inductive = Global.lookup_mind (MutInd.make1 kn) in
- Some (l, SFBmind inductive)
- end @@
- DynHandle.empty
- in
- handle handler o
- | (_,kn), Lib.Leaf Libobject.ModuleObject _ ->
- let mp,l = KerName.repr kn in
- let modl = Global.lookup_module (MPdot (mp, l)) in
- Some (l, SFBmodule modl)
- | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ ->
- let mp,l = KerName.repr kn in
- let modtype = Global.lookup_modtype (MPdot (mp, l)) in
- Some (l, SFBmodtype modtype)
- | (_,kn), Lib.Leaf Libobject.IncludeObject _ ->
- user_err Pp.(str "No extraction of toplevel Include yet.")
- | _ -> None
- in
- List.rev (List.map_filter get_reference (Lib.contents ()))
-
+ List.rev (Safe_typing.structure_body_of_safe_env (Global.safe_env ()))
let environment_until dir_opt =
let rec parse = function
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5ab4409f8b..e2ee5426b5 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -69,18 +69,15 @@ exception FullyUnfocused
let _ = CErrors.register_handler begin function
| CannotUnfocusThisWay ->
- CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way")
+ Pp.str "This proof is focused, but cannot be unfocused this way"
| NoSuchGoals (i,j) when Int.equal i j ->
- CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+ Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
- CErrors.user_err ~hdr:"Focus" Pp.(
- str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
- )
+ Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
| NoSuchGoal id ->
- CErrors.user_err
- ~hdr:"Focus"
- Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
- | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
+ Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+ | FullyUnfocused ->
+ Pp.str "The proof is not focused"
| _ -> raise CErrors.Unhandled
end
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 66e2ae5c29..61e8741973 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -79,7 +79,7 @@ module Strict = struct
(function
| FailedBullet (b,sugg) ->
let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in
- CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg)
+ Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg)
| _ -> raise CErrors.Unhandled)
@@ -204,8 +204,7 @@ exception SuggestNoSuchGoals of int * Proof.t
let _ = CErrors.register_handler begin function
| SuggestNoSuchGoals(n,proof) ->
let suffix = suggest proof in
- CErrors.user_err
- Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
- pr_non_empty_arg (fun x -> x) suffix)
+ Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
+ pr_non_empty_arg (fun x -> x) suffix)
| _ -> raise CErrors.Unhandled
end
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 3c9803432a..a4a06873b8 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -27,7 +27,7 @@ let use_unification_heuristics () = !use_unification_heuristics_ref
exception NoSuchGoal
let () = CErrors.register_handler begin function
- | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
+ | NoSuchGoal -> Pp.(str "No such goal.")
| _ -> raise CErrors.Unhandled
end
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index c81a4abc1b..80b72225f0 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -124,7 +124,7 @@ module Proof_global = struct
let () =
CErrors.register_handler begin function
| NoCurrentProof ->
- CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
+ Pp.(str "No focused proof (No proof-editing in progress).")
| _ -> raise CErrors.Unhandled
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 15:35:48 +0000