aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml2
-rw-r--r--META.coq27
-rw-r--r--Makefile.ci2
-rw-r--r--dev/ci/ci-basic-overlay.sh9
-rwxr-xr-xdev/ci/ci-vst.sh13
-rw-r--r--doc/refman/RefMan-syn.tex2
-rw-r--r--ide/coqOps.ml2
-rw-r--r--ide/ide_slave.ml12
-rw-r--r--ide/wg_ProofView.ml22
-rw-r--r--ide/wg_ProofView.mli2
-rw-r--r--ide/xmlprotocol.ml2
-rw-r--r--kernel/entries.mli2
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/safe_typing.mli9
-rw-r--r--kernel/term_typing.ml67
-rw-r--r--kernel/term_typing.mli12
-rw-r--r--lib/future.ml4
-rw-r--r--library/summary.ml2
-rw-r--r--printing/prettyp.ml8
-rw-r--r--proofs/proof_using.ml2
-rw-r--r--theories/Logic/JMeq.v2
-rw-r--r--theories/Logic/vo.itarget1
-rw-r--r--toplevel/vernac.ml6
-rw-r--r--vernac/vernacentries.ml3
24 files changed, 174 insertions, 51 deletions
diff --git a/.travis.yml b/.travis.yml
index 7138d5c61..81f50af0a 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -40,6 +40,7 @@ env:
- TEST_TARGET="ci-math-comp"
- TEST_TARGET="ci-sf"
- TEST_TARGET="ci-unimath"
+ - TEST_TARGET="ci-vst"
# Not ready yet for 8.7
# - TEST_TARGET="ci-cpdt"
# - TEST_TARGET="ci-metacoq"
@@ -49,6 +50,7 @@ matrix:
allow_failures:
- env: TEST_TARGET="ci-geocoq"
+ - env: TEST_TARGET="ci-vst"
# Full Coq test-suite with two compilers
# [TODO: use yaml refs and avoid duplication for packages list]
diff --git a/META.coq b/META.coq
index 83134d4a0..074c2e457 100644
--- a/META.coq
+++ b/META.coq
@@ -252,6 +252,33 @@ package "highparsing" (
)
+package "idetop" (
+
+ description = "Coq IDE Libraries"
+ version = "8.7"
+
+ requires = "coq.toplevel"
+ directory = "ide"
+
+ archive(byte) = "coqidetop.cma"
+ archive(native) = "coqidetop.cmxa"
+
+)
+
+package "ide" (
+
+ description = "Coq IDE Libraries"
+ version = "8.7"
+
+# XXX Add GTK
+ requires = "coq.toplevel"
+ directory = "ide"
+
+ archive(byte) = "ide.cma"
+ archive(native) = "ide.cmxa"
+
+)
+
package "ltac" (
description = "Coq LTAC Plugin"
diff --git a/Makefile.ci b/Makefile.ci
index 897318c4d..b055ada8e 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,7 +1,7 @@
CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \
ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \
ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \
- ci-unimath
+ ci-unimath ci-vst
.PHONY: $(CI_TARGETS)
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 241ec3586..336ce9d8f 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -46,8 +46,11 @@
########################################################################
# HoTT
########################################################################
+# Temporal overlay
: ${HoTT_CI_BRANCH:=mz-8.7}
: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
+# : ${HoTT_CI_BRANCH:=master}
+# : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}
########################################################################
# GeoCoq
@@ -74,6 +77,12 @@
: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
########################################################################
+# VST
+########################################################################
+: ${VST_CI_BRANCH:=master}
+: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+
+########################################################################
# fiat_parsers
########################################################################
: ${fiat_parsers_CI_BRANCH:=master}
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
new file mode 100755
index 000000000..c11195185
--- /dev/null
+++ b/dev/ci/ci-vst.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+VST_CI_DIR=${CI_BUILD_DIR}/VST
+
+# opam install -j ${NJOBS} -y menhir
+git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR}
+
+# Targets are: msl veric floyd
+# Patch to avoid the upper version limit
+( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} )
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 61093709e..ecaf82806 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -120,7 +120,7 @@ Notation "A \/ B" := (or A B) (at level 85, right associativity).
By default, a notation is considered non associative, but the
precedence level is mandatory (except for special cases whose level is
-canonical). The level is either a number or the mention {\tt next
+canonical). The level is either a number or the phrase {\tt next
level} whose meaning is obvious. The list of levels already assigned
is on Figure~\ref{init-notations}.
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 4a1d688f5..45b5a1007 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -358,7 +358,7 @@ object(self)
| Good evs ->
proof#set_goals goals;
proof#set_evars evs;
- proof#refresh ();
+ proof#refresh ~force:true;
Coq.return ()
)
)
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 2ec79dc58..8cadf1a26 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -79,23 +79,23 @@ let is_undo cmd = match cmd with
| VernacUndo _ | VernacUndoTo _ -> true
| _ -> false
-(** Check whether a command is forbidden by CoqIDE *)
+(** Check whether a command is forbidden in the IDE *)
-let coqide_cmd_checks (loc,ast) =
+let ide_cmd_checks (loc,ast) =
let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in
if is_debug ast then
- user_error "Debug mode not available within CoqIDE";
+ user_error "Debug mode not available in the IDE";
if is_known_option ast then
- Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead");
+ Feedback.msg_warning (strbrk "Set this option from the IDE menu instead");
if Vernac.is_navigation_vernac ast || is_undo ast then
- Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead");
+ Feedback.msg_warning (strbrk "Use IDE navigation instead");
if is_query ast then
Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts")
(** Interpretation (cf. [Ide_intf.interp]) *)
let add ((s,eid),(sid,verbose)) =
- let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in
+ let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in
let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
(* TODO: the "" parameter is a leftover of the times the protocol
* used to include stderr/stdout output.
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index b5405570c..3cbe58388 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -14,7 +14,7 @@ class type proof_view =
object
inherit GObj.widget
method buffer : GText.buffer
- method refresh : unit -> unit
+ method refresh : force:bool -> unit
method clear : unit -> unit
method set_goals : Interface.goals option -> unit
method set_evars : Interface.evar list option -> unit
@@ -197,6 +197,7 @@ let proof_view () =
inherit GObj.widget view#as_widget
val mutable goals = None
val mutable evars = None
+ val mutable last_width = -1
method buffer = text_buffer
@@ -206,13 +207,24 @@ let proof_view () =
method set_evars evs = evars <- evs
- method refresh () =
- let dummy _ () = () in
- display (mode_tactic dummy) view goals None evars
+ method refresh ~force =
+ (* We need to block updates here due to the following race:
+ insertion of messages may create a vertical scrollbar, this
+ will trigger a width change, calling refresh again and
+ going into an infinite loop. *)
+ let width = Ideutils.textview_width view in
+ (* Could still this method race if the scrollbar changes the
+ textview_width ?? *)
+ let needed = force || last_width <> width in
+ if needed then begin
+ last_width <- width;
+ let dummy _ () = () in
+ display (mode_tactic dummy) view goals None evars
+ end
end
in
(* Is there a better way to connect the signal ? *)
(* Can this be done in the object constructor? *)
- let w_cb _ = pf#refresh () in
+ let w_cb _ = pf#refresh ~force:false in
ignore (view#misc#connect#size_allocate w_cb);
pf
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index aa01d955d..a90d429d0 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -10,7 +10,7 @@ class type proof_view =
object
inherit GObj.widget
method buffer : GText.buffer
- method refresh : unit -> unit
+ method refresh : force:bool -> unit
method clear : unit -> unit
method set_goals : Interface.goals option -> unit
method set_evars : Interface.evar list option -> unit
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 5f80d6897..d7950e5fd 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -111,7 +111,7 @@ let to_box = let open Pp in
)
let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with
- | Ppcmd_empty -> constructor "ppdoc" "emtpy" []
+ | Ppcmd_empty -> constructor "ppdoc" "empty" []
| Ppcmd_string s -> constructor "ppdoc" "string" [of_string s]
| Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl]
| Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)]
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 77081947e..1e07c9690 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -113,5 +113,3 @@ type side_effect = {
from_env : Declarations.structure_body CEphemeron.key;
eff : side_eff;
}
-
-type side_effects = side_effect list
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2312f891c..caaaff1b8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -208,19 +208,19 @@ let get_opaque_body env cbo =
Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
type private_constant = Entries.side_effect
-type private_constants = private_constant list
+type private_constants = Term_typing.side_effects
type private_constant_role = Term_typing.side_effect_role =
| Subproof
| Schema of inductive * string
-let empty_private_constants = []
-let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs
-let concat_private xs ys = List.fold_right add_private xs ys
+let empty_private_constants = Term_typing.empty_seff
+let add_private = Term_typing.add_seff
+let concat_private = Term_typing.concat_seff
let mk_pure_proof = Term_typing.mk_pure_proof
let inline_private_constants_in_constr = Term_typing.inline_side_effects
let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
-let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
+let side_effects_of_private_constants = Term_typing.uniq_seff
let private_con_of_con env c =
let cbo = Environ.lookup_constant c env.env in
@@ -250,7 +250,7 @@ let universes_of_private eff =
| Entries.SEsubproof (c, cb, e) ->
if cb.const_polymorphic then acc
else Univ.ContextSet.of_context cb.const_universes :: acc)
- [] eff
+ [] (Term_typing.uniq_seff eff)
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 15ebc7d88..efeb98bd2 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -47,11 +47,18 @@ type private_constant_role =
| Schema of inductive * string
val side_effects_of_private_constants :
- private_constants -> Entries.side_effects
+ private_constants -> Entries.side_effect list
+(** Return the list of individual side-effects in the order of their
+ creation. *)
val empty_private_constants : private_constants
val add_private : private_constant -> private_constants -> private_constants
+(** Add a constant to a list of private constants. The former must be more
+ recent than all constants appearing in the latter, i.e. one should not
+ create a dependency cycle. *)
val concat_private : private_constants -> private_constants -> private_constants
+(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
+ [e1] must be more recent than those of [e2]. *)
val private_con_of_con : safe_environment -> constant -> private_constant
val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 569a58378..2eb2c040e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -26,8 +26,6 @@ module NamedDecl = Context.Named.Declaration
(* Insertion of constants and parameters in environment. *)
-let mk_pure_proof c = (c, Univ.ContextSet.empty), []
-
let equal_eff e1 e2 =
let open Entries in
match e1, e2 with
@@ -39,13 +37,54 @@ let equal_eff e1 e2 =
cl1 cl2
| _ -> false
-let rec uniq_seff = function
- | [] -> []
- | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
-(* The list of side effects is in reverse order (most recent first).
- * To keep the "topological" order between effects we have to uniq-ize from
- * the tail *)
-let uniq_seff l = List.rev (uniq_seff (List.rev l))
+module SideEffects :
+sig
+ type t
+ val repr : t -> side_effect list
+ val empty : t
+ val add : side_effect -> t -> t
+ val concat : t -> t -> t
+end =
+struct
+
+let compare_seff e1 e2 = match e1, e2 with
+| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2
+| SEscheme (cl1, _), SEscheme (cl2, _) ->
+ let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in
+ CList.compare cmp cl1 cl2
+| SEsubproof _, SEscheme _ -> -1
+| SEscheme _, SEsubproof _ -> 1
+
+module SeffOrd = struct
+type t = side_effect
+let compare e1 e2 = compare_seff e1.eff e2.eff
+end
+
+module SeffSet = Set.Make(SeffOrd)
+
+type t = { seff : side_effect list; elts : SeffSet.t }
+(** Invariant: [seff] is a permutation of the elements of [elts] *)
+
+let repr eff = eff.seff
+let empty = { seff = []; elts = SeffSet.empty }
+let add x es =
+ if SeffSet.mem x es.elts then es
+ else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
+let concat xes yes =
+ List.fold_right add xes.seff yes
+
+end
+
+type side_effects = SideEffects.t
+
+let uniq_seff_rev = SideEffects.repr
+let uniq_seff l = List.rev (SideEffects.repr l)
+
+let empty_seff = SideEffects.empty
+let add_seff = SideEffects.add
+let concat_seff = SideEffects.concat
+
+let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
let inline_side_effects env body ctx side_eff =
let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
@@ -98,7 +137,7 @@ let inline_side_effects env body ctx side_eff =
t, ctx, (mb,List.length cbl) :: sl
in
(* CAVEAT: we assure a proper order *)
- List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+ List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff)
(* Given the list of signatures of side effects, checks if they match.
* I.e. if they are ordered descendants of the current revstruct *)
@@ -380,7 +419,7 @@ let constant_entry_of_side_effect cb u =
| Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
| _ -> assert false in
DefinitionEntry {
- const_entry_body = Future.from_val (pt, []);
+ const_entry_body = Future.from_val (pt, empty_seff);
const_entry_secctx = None;
const_entry_feedback = None;
const_entry_type =
@@ -414,7 +453,7 @@ let export_side_effects mb env ce =
let _, eff = Future.force body in
let ce = DefinitionEntry { c with
const_entry_body = Future.chain ~pure:true body
- (fun (b_ctx, _) -> b_ctx, []) } in
+ (fun (b_ctx, _) -> b_ctx, empty_seff) } in
let not_exists (c,_,_,_) =
try ignore(Environ.lookup_constant c env); false
with Not_found -> true in
@@ -426,7 +465,7 @@ let export_side_effects mb env ce =
let cbl = List.filter not_exists cbl in
if cbl = [] then acc, sl
else cbl :: acc, (mb,List.length cbl) :: sl in
- let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
+ let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in
let trusted = check_signatures mb signatures in
let push_seff env = function
| kn, cb, `Nothing, _ ->
@@ -498,7 +537,7 @@ let inline_entry_side_effects env ce = { ce with
const_entry_body = Future.chain ~pure:true
ce.const_entry_body (fun ((body, ctx), side_eff) ->
let body, ctx',_ = inline_side_effects env body ctx side_eff in
- (body, ctx'), []);
+ (body, ctx'), empty_seff);
}
let inline_side_effects env body side_eff =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 89b5fc40e..075389ea5 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,6 +12,8 @@ open Environ
open Declarations
open Entries
+type side_effects
+
val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
constant_def * types * constant_universes
@@ -29,7 +31,15 @@ val inline_entry_side_effects :
{!Entries.const_entry_body} field. It is meant to get a term out of a not
yet type checked proof. *)
-val uniq_seff : side_effects -> side_effects
+val empty_seff : side_effects
+val add_seff : side_effect -> side_effects -> side_effects
+val concat_seff : side_effects -> side_effects -> side_effects
+(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in
+ [e1] must be more recent than those of [e2]. *)
+val uniq_seff : side_effects -> side_effect list
+(** Return the list of individual side-effects in the order of their
+ creation. *)
+
val equal_eff : side_effect -> side_effect -> bool
val translate_constant :
diff --git a/lib/future.ml b/lib/future.ml
index b60b32bb6..1360b7ac4 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -151,8 +151,8 @@ let chain ~pure ck f =
create ~uuid ~name fix_exn (match !c with
| Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck))
| Exn _ as x -> x
- | Val (v, None) when pure -> Closure (fun () -> f v)
- | Val (v, Some _) when pure -> Closure (fun () -> f v)
+ | Val (v, None) when pure -> Val (f v, None)
+ | Val (v, Some _) when pure -> Val (f v, None)
| Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
| Val (v, None) ->
match !ck with
diff --git a/library/summary.ml b/library/summary.ml
index 2ec4760d6..d9f644100 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -108,7 +108,7 @@ let unfreeze_summaries fs =
with e when CErrors.noncritical e ->
let e = CErrors.push e in
Feedback.msg_error
- Pp.(seq [str "Error unfrezing summay %s\n%s\n%!";
+ Pp.(seq [str "Error unfreezing summary %s\n%s\n%!";
str (name_of_summary id);
CErrors.iprint e]);
iraise e
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8fabb7053..5963d45ef 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -204,6 +204,11 @@ let print_opacity ref =
str "transparent (with minimal expansion weight)"]
(*******************)
+
+let print_if_is_coercion ref =
+ if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else []
+
+(*******************)
(* *)
let print_polymorphism ref =
@@ -257,7 +262,8 @@ let print_name_infos ref =
type_info_for_implicit @
print_renames_list (mt()) renames @
print_impargs_list (mt()) impls @
- print_argument_scopes (mt()) scopes
+ print_argument_scopes (mt()) scopes @
+ print_if_is_coercion ref
let print_id_args_data test pr id l =
if List.exists test l then
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f51586c73..2c489d6de 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids =
let suggest_Proof_using name env vars ids_typ context_ids =
let module S = Id.Set in
let open Pp in
- let print x = Feedback.msg_error x in
+ let print x = Feedback.msg_debug x in
let pr_set parens s =
let wrap ppcmds =
if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 2f95856b4..86d05e8fb 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -130,7 +130,7 @@ Qed.
is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *)
Lemma JMeq_eq_dep :
- forall U (P:U->Prop) p q (x:P p) (y:P q),
+ forall U (P:U->Type) p q (x:P p) (y:P q),
p = q -> JMeq x y -> eq_dep U P p x q y.
Proof.
intros.
diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget
index 8b0aa6691..5eba0b623 100644
--- a/theories/Logic/vo.itarget
+++ b/theories/Logic/vo.itarget
@@ -27,6 +27,7 @@ IndefiniteDescription.vo
JMeq.vo
ProofIrrelevanceFacts.vo
ProofIrrelevance.vo
+PropFacts.vo
PropExtensionality.vo
RelationalChoice.vo
SetIsType.vo
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 06908abb6..9917a49b4 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -266,9 +266,9 @@ let ensure_bname src tgt =
let src, tgt = Filename.basename src, Filename.basename tgt in
let src, tgt = chop_extension src, chop_extension tgt in
if src <> tgt then begin
- Feedback.msg_error (str "Source and target file names must coincide, directories can differ");
- Feedback.msg_error (str "Source: " ++ str src);
- Feedback.msg_error (str "Target: " ++ str tgt);
+ Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
+ str "Source: " ++ str src ++ fnl () ++
+ str "Target: " ++ str tgt);
flush_all ();
exit 1
end
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 64c06d77a..ca03ba3f3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -67,8 +67,7 @@ let show_node () =
could, possibly, be cleaned away. (Feb. 2010) *)
()
-let show_thesis () =
- Feedback.msg_error (anomaly (Pp.str "TODO") )
+let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO")
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 14:25:43 +0000