aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore1
-rw-r--r--kernel/nativecode.ml24
-rw-r--r--ltac/profile_ltac.ml6
-rw-r--r--pretyping/typeclasses.ml6
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--printing/pptactic.ml25
-rw-r--r--proofs/clenvtac.ml26
-rw-r--r--test-suite/Makefile49
-rw-r--r--test-suite/bugs/closed/PLACEHOLDER.v0
-rw-r--r--test-suite/bugs/closed/bug_4836.v1
-rw-r--r--test-suite/bugs/closed/bug_4836/PLACEHOLDER0
-rw-r--r--test-suite/output-modulo-time/ltacprof.out12
-rw-r--r--test-suite/output-modulo-time/ltacprof.v8
-rw-r--r--test-suite/output/Errors.out2
-rw-r--r--test-suite/output/ltac.out17
-rw-r--r--toplevel/coqinit.ml3
16 files changed, 141 insertions, 41 deletions
diff --git a/.gitignore b/.gitignore
index 8a0c54f8fe..4acd9930e3 100644
--- a/.gitignore
+++ b/.gitignore
@@ -54,6 +54,7 @@ kernel/byterun/dllcoqrun.so
coqdoc.sty
csdp.cache
test-suite/lia.cache
+test-suite/nra.cache
test-suite/trace
test-suite/misc/universes/all_stdlib.v
test-suite/misc/universes/universes.txt
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 87302dcf5a..ad5b04f3d1 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -22,8 +22,12 @@ to OCaml code. *)
(** Local names **)
+(* The first component is there for debugging purposes only *)
type lname = { lname : name; luid : int }
+let eq_lname ln1 ln2 =
+ Int.equal ln1.luid ln2.luid
+
let dummy_lname = { lname = Anonymous; luid = -1 }
module LNord =
@@ -82,6 +86,9 @@ let eq_gname gn1 gn2 =
| Gnamed id1, Gnamed id2 -> Id.equal id1 id2
| _ -> false
+let dummy_gname =
+ Grel 0
+
open Hashset.Combine
let gname_hash gn = match gn with
@@ -404,9 +411,13 @@ let opush_lnames n env lns =
let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
match t1, t2 with
| MLlocal ln1, MLlocal ln2 ->
+ (try
Int.equal (LNmap.find ln1 env1) (LNmap.find ln2 env2)
+ with Not_found ->
+ eq_lname ln1 ln2)
| MLglobal gn1', MLglobal gn2' ->
eq_gname gn1' gn2' || (eq_gname gn1 gn1' && eq_gname gn2 gn2')
+ || (eq_gname gn1 gn2' && eq_gname gn2 gn1')
| MLprimitive prim1, MLprimitive prim2 -> eq_primitive prim1 prim2
| MLlam (lns1, ml1), MLlam (lns2, ml2) ->
Int.equal (Array.length lns1) (Array.length lns2) &&
@@ -719,6 +730,11 @@ let push_global_norm gn params body =
let push_global_case gn params annot a accu bs =
push_global gn (Gletcase (gn, params, annot, a, accu, bs))
+(* Compares [t1] and [t2] up to alpha-equivalence. [t1] and [t2] may contain
+ free variables. *)
+let eq_mllambda t1 t2 =
+ eq_mllambda dummy_gname dummy_gname 0 LNmap.empty LNmap.empty t1 t2
+
(*s Compilation environment *)
type env =
@@ -897,9 +913,7 @@ let rec insert cargs body rl =
let params = rm_params fv params in
rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
| Rcons(l,fv,body',rl) ->
- (** ppedrot: It seems we only want to factorize common branches. It should
- not matter to do so with a subapproximation by (==). *)
- if body == body' then
+ if eq_mllambda body body' then
let (c,params) = cargs in
let params = rm_params fv params in
l := (c,params)::!l
@@ -1446,12 +1460,14 @@ let optimize gdef l =
end
| MLif(t,b1,b2) ->
+ (* This optimization is critical: it applies to all fixpoints that start
+ by matching on their recursive argument *)
let t = optimize s t in
let b1 = optimize s b1 in
let b2 = optimize s b2 in
begin match t, b2 with
| MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs)
- when l1 == l2 -> MLmatch(annot, l1, b1, bs) (** approximation *)
+ when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs)
| _, _ -> MLif(t, b1, b2)
end
| MLmatch(annot,a,accu,bs) ->
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index 3661fe54f2..d2b7c70750 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -147,7 +147,7 @@ let rec list_iter_is_last f = function
| x :: xs -> f false x :: list_iter_is_last f xs
let header =
- str " tactic local total calls max" ++
+ str " tactic local total calls max " ++
fnl () ++
str "────────────────────────────────────────┴──────┴──────┴───────┴─────────┘" ++
fnl ()
@@ -160,6 +160,7 @@ let rec print_node ~filter all_total indent prefix (s, e) =
++ padl 8 (string_of_int e.ncalls)
++ padl 10 (format_sec (e.max_total))
) ++
+ fnl () ++
print_table ~filter all_total indent false e.children
and print_table ~filter all_total indent first_level table =
@@ -179,7 +180,7 @@ and print_table ~filter all_total indent first_level table =
let sep1 = if first_level then "─" else if is_last then " └─" else " ├─" in
print_node ~filter all_total (indent ^ sep0) (indent ^ sep1)
in
- prlist_with_sep fnl (fun pr -> pr) (list_iter_is_last iter ls)
+ prlist (fun pr -> pr) (list_iter_is_last iter ls)
let to_string ~filter node =
let tree = node.children in
@@ -224,7 +225,6 @@ let to_string ~filter node =
header ++
print_table ~filter all_total "" true flat_tree ++
fnl () ++
- fnl () ++
header ++
print_table ~filter all_total "" true tree
in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2c675b9eae..31ef3dfdd7 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -501,7 +501,7 @@ let is_resolvable evi =
Option.is_empty (Store.get evi.evar_extra resolvable)
let mark_resolvability_undef b evi =
- if is_resolvable evi = b then evi
+ if is_resolvable evi == (b : bool) then evi
else
let t = set_resolvable evi.evar_extra b in
{ evi with evar_extra = t }
@@ -548,7 +548,7 @@ let solve_all_instances env evd filter unique split fail =
(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *)
-let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
+let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
?(split=true) ?(fail=true) env evd =
- if not (has_typeclasses filter evd) then evd
+ if fast_path && not (has_typeclasses filter evd) then evd
else solve_all_instances env evd filter unique split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 25460ef7d3..2530f5dfae 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -101,7 +101,7 @@ val mark_resolvable : evar_info -> evar_info
val is_class_evar : evar_map -> evar_info -> bool
val is_class_type : evar_map -> types -> bool
-val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool ->
+val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 917a277c91..e2c78a5075 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -373,20 +373,25 @@ module Make
in
str "<" ++ name ++ str ">" ++ args
+ let rec pr_user_symbol = function
+ | Extend.Ulist1 tkn -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist1sep (tkn, _) -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist0 tkn -> pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist0sep (tkn, _) -> pr_user_symbol tkn ^ "_list"
+ | Extend.Uopt tkn -> pr_user_symbol tkn ^ "_opt"
+ | Extend.Uentry tag ->
+ let ArgT.Any tag = tag in
+ ArgT.repr tag
+ | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl
+
let pr_alias_key key =
try
let prods = (KNmap.find key !prnotation_tab).pptac_prods in
- (* First printing strategy: only the head symbol *)
- match prods with
- | TacTerm s :: prods -> str s
- | _ ->
- (* Second printing strategy; if ever Tactic Notation is eventually *)
- (* accepting notations not starting with an identifier *)
let rec pr = function
- | [] -> []
- | TacTerm s :: prods -> s :: pr prods
- | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in
- str (String.concat " " (pr prods))
+ | TacTerm s -> primitive s
+ | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
+ in
+ pr_sequence pr prods
with Not_found ->
KerName.print key
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 04a2eb4879..98b5bc8b05 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -59,6 +59,19 @@ let clenv_pose_dependent_evars with_evars clenv =
(RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
clenv_pose_metas_as_evars clenv dep_mvs
+(** Use our own fast path, more informative than from Typeclasses *)
+let check_tc evd =
+ let has_resolvable = ref false in
+ let check _ evi =
+ let res = Typeclasses.is_resolvable evi in
+ if res then
+ let () = has_resolvable := true in
+ Typeclasses.is_class_evar evd evi
+ else false
+ in
+ let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
+ (has_typeclass, !has_resolvable)
+
let clenv_refine with_evars ?(with_classes=true) clenv =
(** ppedrot: a Goal.enter here breaks things, because the tactic below may
solve goals by side effects, while the compatibility layer keeps those
@@ -67,9 +80,16 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
let clenv = clenv_pose_dependent_evars with_evars clenv in
let evd' =
if with_classes then
- let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
- ~fail:(not with_evars) clenv.env clenv.evd
- in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
+ let (has_typeclass, has_resolvable) = check_tc clenv.evd in
+ let evd' =
+ if has_typeclass then
+ Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
+ ~fail:(not with_evars) clenv.env clenv.evd
+ else clenv.evd
+ in
+ if has_resolvable then
+ Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
+ else evd'
else clenv.evd
in
let clenv = { clenv with evd = evd' } in
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 81321729d4..a3050bfccc 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -49,6 +49,10 @@ SINGLE_QUOTE="
#" # double up on the quotes, in a comment, to appease the emacs syntax highlighter
# wrap the arguments in parens, but only if they exist
get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
+# get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
+has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
+has_profile_ltac_or_compile_flag = $(filter "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
+get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command))
bogomips:=
@@ -79,7 +83,7 @@ COMPLEXITY := $(if $(bogomips),complexity)
BUGS := bugs/opened bugs/closed
VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
- interactive micromega $(COMPLEXITY) modules stm
+ output-modulo-time interactive micromega $(COMPLEXITY) modules stm
# All subsystems
SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
@@ -133,6 +137,7 @@ summary:
$(call summary_dir, "Failure tests", failure); \
$(call summary_dir, "Bugs tests", bugs); \
$(call summary_dir, "Output tests", output); \
+ $(call summary_dir, "Output (modulo time changes) tests", output-modulo-time); \
$(call summary_dir, "Interactive tests", interactive); \
$(call summary_dir, "Micromega tests", micromega); \
$(call summary_dir, "Miscellaneous tests", misc); \
@@ -172,7 +177,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...still active"; \
@@ -193,7 +198,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -226,7 +231,7 @@ $(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.
$(HIDE){ \
opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -256,7 +261,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
@@ -271,7 +276,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
$(HIDE){ \
echo $(call log_intro,$<); \
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
| grep -v "Welcome to Coq" \
| grep -v "\[Loading ML file" \
| grep -v "Skipping rcfile loading" \
@@ -288,6 +293,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
rm $$tmpoutput; \
} > "$@"
+$(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
+ $(HIDE){ \
+ echo $(call log_intro,$<); \
+ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+ tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
+ | grep -v "Welcome to Coq" \
+ | grep -v "\[Loading ML file" \
+ | grep -v "Skipping rcfile loading" \
+ | grep -v "^<W>" \
+ | sed 's/\s*[0-9]*\.[0-9]\+\s*//g' \
+ | sed 's/\s*0\.\s*//g' \
+ > $$tmpoutput; \
+ sed 's/\s*[0-9]*\.[0-9]\+\s*//g' $*.out | sed 's/\s*0\.\s*//g' > $$tmpexpected; \
+ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \
+ if [ $$R = 0 ]; then \
+ echo $(log_success); \
+ echo " $<...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " $<...Error! (unexpected output)"; \
+ fi; \
+ rm $$tmpoutput; \
+ rm $$tmpexpected; \
+ } > "$@"
+
$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
@@ -311,7 +343,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
$(HIDE){ \
echo $(call log_intro,$<); \
true "extract effective user time"; \
- res=`$(command) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
+ res=`$(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \
R=$$?; times; \
if [ $$R != 0 ]; then \
echo $(log_failure); \
@@ -341,7 +373,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- $(command) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+ $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
if [ $$R != 0 ]; then \
echo $(log_success); \
echo " $<...still wished"; \
@@ -483,4 +515,3 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
echo " $<...Error!"; \
fi; \
} > "$@"
-
diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/bugs/closed/PLACEHOLDER.v
diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v
new file mode 100644
index 0000000000..5838dcd8a7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4836.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *)
diff --git a/test-suite/bugs/closed/bug_4836/PLACEHOLDER b/test-suite/bugs/closed/bug_4836/PLACEHOLDER
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4836/PLACEHOLDER
diff --git a/test-suite/output-modulo-time/ltacprof.out b/test-suite/output-modulo-time/ltacprof.out
new file mode 100644
index 0000000000..cc04c2c9bd
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof.out
@@ -0,0 +1,12 @@
+total time: 1.528s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0% 1 1.528s
+─constructor --------------------------- 0.0% 0.0% 1 0.000s
+
+ tactic local total calls max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─sleep' -------------------------------- 100.0% 100.0% 1 1.528s
+─constructor --------------------------- 0.0% 0.0% 1 0.000s
+
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v
new file mode 100644
index 0000000000..d79451f0f7
--- /dev/null
+++ b/test-suite/output-modulo-time/ltacprof.v
@@ -0,0 +1,8 @@
+(* -*- coq-prog-args: ("-emacs" "-profile-ltac") -*- *)
+Ltac sleep' := do 100 (do 100 (do 100 idtac)).
+Ltac sleep := sleep'.
+
+Theorem x : True.
+Proof.
+ idtac. idtac. sleep. constructor.
+Defined.
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 62e9ef4b20..06a6b2d157 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -6,5 +6,5 @@ The command has indeed failed with message:
In nested Ltac calls to "f" and "apply x", last call failed.
Unable to unify "nat" with "True".
The command has indeed failed with message:
-Ltac call to "instantiate" failed.
+Ltac call to "instantiate ( (ident) := (lglob) )" failed.
Error: Instance is not well-typed in the environment of ?x.
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 21554e9ff8..f4254e4e2f 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -4,20 +4,25 @@ Ltac f x y z :=
symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
dependent z
The command has indeed failed with message:
-In nested Ltac calls to "g1" and "refine", last call failed.
+In nested Ltac calls to "g1" and "refine (uconstr)", last call failed.
The term "I" has type "True" while it is expected to have type "False".
The command has indeed failed with message:
-In nested Ltac calls to "f1" and "refine", last call failed.
+In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call
+failed.
The term "I" has type "True" while it is expected to have type "False".
The command has indeed failed with message:
-In nested Ltac calls to "g2", "g1" and "refine", last call failed.
+In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call
+failed.
The term "I" has type "True" while it is expected to have type "False".
The command has indeed failed with message:
-In nested Ltac calls to "f2", "f1" and "refine", last call failed.
+In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call
+failed.
The term "I" has type "True" while it is expected to have type "False".
The command has indeed failed with message:
-In nested Ltac calls to "h" and "injection", last call failed.
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
Error: No primitive equality found.
The command has indeed failed with message:
-In nested Ltac calls to "h" and "injection", last call failed.
+In nested Ltac calls to "h" and "injection (destruction_arg)", last call
+failed.
Error: No primitive equality found.
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 258a1135fc..8a8dbe9601 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -89,7 +89,8 @@ let init_load_path () =
Mltop.add_ml_dir (coqlib/"stm");
Mltop.add_ml_dir (coqlib/"ide")
end;
- Mltop.add_ml_dir (coqlib/"toploop");
+ if System.exists_dir (coqlib/"toploop") then
+ Mltop.add_ml_dir (coqlib/"toploop");
(* then standard library *)
add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
(* then plugins *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:57:58 +0000