aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/04-tactics/12399-rm-prolog.rst4
-rw-r--r--doc/changelog/08-tools/12389-coq_makefile.rst5
-rw-r--r--doc/sphinx/practical-tools/utilities.rst4
-rw-r--r--plugins/ltac/g_auto.mlg5
-rw-r--r--plugins/ssrsearch/g_search.mlg2
-rw-r--r--tactics/eauto.ml25
-rw-r--r--tactics/eauto.mli2
-rw-r--r--test-suite/output/ErrorLocation_12152_1.v1
-rw-r--r--test-suite/output/ErrorLocation_12152_2.v1
-rw-r--r--test-suite/output/ErrorLocation_12255.v1
-rw-r--r--tools/CoqMakefile.in28
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg2
-rw-r--r--vernac/mltop.ml3
13 files changed, 39 insertions, 44 deletions
diff --git a/doc/changelog/04-tactics/12399-rm-prolog.rst b/doc/changelog/04-tactics/12399-rm-prolog.rst
new file mode 100644
index 0000000000..afde7db370
--- /dev/null
+++ b/doc/changelog/04-tactics/12399-rm-prolog.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+ The deprecated and undocumented "prolog" tactic was removed
+ (`#12399 <https://github.com/coq/coq/pull/12399>`_,
+ by Pierre-Marie Pédrot).
diff --git a/doc/changelog/08-tools/12389-coq_makefile.rst b/doc/changelog/08-tools/12389-coq_makefile.rst
new file mode 100644
index 0000000000..74e3a68170
--- /dev/null
+++ b/doc/changelog/08-tools/12389-coq_makefile.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+ Adding the possibility in coq_makefile to directly set the installation folders,
+ through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables.
+ See :ref:`coqmakefilelocal`.
+ (`#12389 <https://github.com/coq/coq/pull/12389>`_, by Martin Bodin, review of Enrico Tassi).
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 408f8fc3ec..33ebbce640 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -170,6 +170,10 @@ Here we describe only few of them.
override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``.
:COQDOCEXTRAFLAGS:
extend the flags passed to ``coqdoc``
+:COQLIBINSTALL, COQDOCINSTALL:
+ specify where the Coq libraries and documentation will be installed.
+ By default a combination of ``$(DESTDIR)`` (if defined) with
+ ``$(COQLIB)/user-contrib`` and ``$(DOCDIR)/user-contrib``.
**Rule extension**
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index b4527694ae..2e72ceae5a 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -114,11 +114,6 @@ END
(** Eauto *)
-TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () }
-| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] ->
- { Eauto.prolog_tac (eval_uconstrs ist l) n }
-END
-
{
let make_depth n = snd (Eauto.make_dimension n None)
diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg
index 6d68cc13ab..f5cbf2005b 100644
--- a/plugins/ssrsearch/g_search.mlg
+++ b/plugins/ssrsearch/g_search.mlg
@@ -2,6 +2,8 @@
(* Main prefilter *)
+DECLARE PLUGIN "ssrsearch_plugin"
+
{
module CoqConstr = Constr
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 710e0a6808..7d8620468d 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -77,31 +77,6 @@ let apply_tac_list tac glls =
re_sig (pack.it @ rest) pack.sigma
| _ -> user_err Pp.(str "apply_tac_list")
-let one_step l gl =
- [Proofview.V82.of_tactic Tactics.intro]
- @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
- @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
- @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
-
-let rec prolog l n gl =
- if n <= 0 then user_err Pp.(str "prolog - failure");
- let prol = (prolog l (n-1)) in
- (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
-
-let prolog_tac l n =
- Proofview.V82.tactic begin fun gl ->
- let map c =
- let (sigma, c) = c (pf_env gl) (project gl) in
- (* Dropping the universe context is probably wrong *)
- let (c, _) = pf_apply (prepare_hint false) gl (sigma, c) in
- c
- in
- let l = List.map map l in
- try (prolog l n gl)
- with UserError (Some "Refiner.tclFIRST",_) ->
- user_err ~hdr:"Prolog.prolog" (str "Prolog failed.")
- end
-
open Auto
(***************************************************************************)
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e6f2c1a8e2..5fb038a767 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -18,8 +18,6 @@ val registered_e_assumption : unit Proofview.tactic
val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
-val prolog_tac : delayed_open_constr list -> int -> unit Proofview.tactic
-
val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list ->
hint_db_name list option -> unit Proofview.tactic
diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v
index e63ab1cd48..709ac305e4 100644
--- a/test-suite/output/ErrorLocation_12152_1.v
+++ b/test-suite/output/ErrorLocation_12152_1.v
@@ -1,3 +1,4 @@
(* Reported in #12152 *)
Goal True.
intro H; auto.
+Abort.
diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v
index 5df6bec939..29e4c910d8 100644
--- a/test-suite/output/ErrorLocation_12152_2.v
+++ b/test-suite/output/ErrorLocation_12152_2.v
@@ -1,3 +1,4 @@
(* Reported in #12152 *)
Goal True.
intros H; auto.
+Abort.
diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v
index 347424b2fc..59c0e1dfc5 100644
--- a/test-suite/output/ErrorLocation_12255.v
+++ b/test-suite/output/ErrorLocation_12255.v
@@ -2,3 +2,4 @@ Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac.
Definition i := O.
Goal False.
can_unfold (i>0).
+Abort.
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index a26eb9dfbe..e2ed2db728 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -146,6 +146,21 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
TGTS ?=
+# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
+ifdef DSTROOT
+DESTDIR := $(DSTROOT)
+endif
+
+# Substitution of the path by appending $(DESTDIR) if needed.
+# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments.
+windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1))
+destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1))
+
+# Installation paths of libraries and documentation.
+COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib)
+COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib)
+COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable?
+
########## End of parameters ##################################################
# What follows may be relevant to you only if you need to
# extend this Makefile. If so, look for 'Extension point' here and
@@ -227,17 +242,6 @@ else
TIMING_ARG=
endif
-# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not)
-ifdef DSTROOT
-DESTDIR := $(DSTROOT)
-endif
-
-concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2))
-
-COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib)
-COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib)
-COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
-
# Files #######################################################################
#
# We here define a bunch of variables about the files being part of the
@@ -577,7 +581,7 @@ uninstall::
instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\
rm -f "$$instf" &&\
echo RM "$$instf" &&\
- (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \
+ (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \
done
.PHONY: uninstall
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 8979170026..3af39ec59a 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+DECLARE PLUGIN "ltac2_plugin"
+
{
open Pp
diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index d276a1ac35..c33b3d29f8 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -309,6 +309,9 @@ type ml_module_object = {
}
let add_module_digest m =
+ if not has_dynlink then
+ m, NoDigest
+ else
try
let file = file_of_name m in
let path, file = System.where_in_path ~warn:false !coq_mlpath_copy file in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 10:47:35 +0000