aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.ide6
-rw-r--r--checker/checker.ml21
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh4
-rw-r--r--doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst5
-rw-r--r--doc/changelog/08-tools/12613-coqchk-noi.rst3
-rw-r--r--tactics/tactics.ml18
-rw-r--r--test-suite/ltac2/syntax.v12
-rw-r--r--tools/CoqMakefile.in2
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg10
9 files changed, 40 insertions, 41 deletions
diff --git a/Makefile.ide b/Makefile.ide
index 640ee7b188..789acee5ec 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -296,10 +296,12 @@ $(COQIDEAPP):$(COQIDEAPP)/Contents/Resources
# CoqIde for Windows special targets
###########################################################################
+# This is either x86_64-w64-mingw32 or i686-w64-mingw32
+TARGET_ARCH=$(shell $CC -dumpmachine)
+
%.o: %.rc
$(SHOW)'WINDRES $<'
- $(HIDE)i686-w64-mingw32-windres -i $< -o $@
-
+ $(HIDE)$(TARGET_ARCH)-windres -i $< -o $@
# For emacs:
# Local Variables:
diff --git a/checker/checker.ml b/checker/checker.ml
index ab0ea41a36..e2c90e2b93 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -95,12 +95,10 @@ let add_rec_path ~unix_path ~coq_root =
else
Feedback.msg_warning (str "Cannot open " ++ str unix_path)
-(* By the option -include -I or -R of the command line *)
+(* By the option -R/-Q of the command line *)
let includes = ref []
let push_include (s, alias) = includes := (s,alias) :: !includes
-let set_default_include d =
- push_include (d, Check.default_root_prefix)
let set_include d p =
let p = dirpath_of_string p in
push_include (d,p)
@@ -127,7 +125,7 @@ let init_load_path () =
List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
(* then current directory *)
add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
- (* additional loadpath, given with -I -include -R options *)
+ (* additional loadpath, given with -R/-Q options *)
List.iter
(fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root)
(List.rev !includes);
@@ -321,9 +319,6 @@ let explain_exn = function
report ())
| e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
-let deprecated flag =
- Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag))
-
let parse_args argv =
let rec parse = function
| [] -> ()
@@ -339,16 +334,8 @@ let parse_args argv =
Envars.set_user_coqlib s;
parse rem
- | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem
- | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
- | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem
- | ("-I"|"-include") :: [] -> usage ()
-
- | "-Q" :: d :: p :: rem -> set_include d p;parse rem
- | "-Q" :: ([] | [_]) -> usage ()
-
- | "-R" :: d :: p :: rem -> set_include d p;parse rem
- | "-R" :: ([] | [_]) -> usage ()
+ | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem
+ | ("-Q"|"-R") :: ([] | [_]) -> usage ()
| "-debug" :: rem -> set_debug (); parse rem
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 6ceb7f54b2..cc9fd13fdc 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1401,10 +1401,6 @@ function make_coq {
logn configure ./configure -with-doc no -prefix "$PREFIXCOQ"
fi
- # The windows resource compiler binary name is hard coded
- sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build
- sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.ide || true
-
# 8.4x doesn't support parallel make
if [[ $COQ_VERSION == 8.4* ]] ; then
log1 make
diff --git a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst
new file mode 100644
index 0000000000..555020d319
--- /dev/null
+++ b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+ Fix the parsing of multi-parameters Ltac2 types
+ (`#12594 <https://github.com/coq/coq/pull/12594>`_,
+ fixes `#12595 <https://github.com/coq/coq/issues/12595>`_,
+ by Pierre-Marie Pédrot).
diff --git a/doc/changelog/08-tools/12613-coqchk-noi.rst b/doc/changelog/08-tools/12613-coqchk-noi.rst
new file mode 100644
index 0000000000..b83c9c69a2
--- /dev/null
+++ b/doc/changelog/08-tools/12613-coqchk-noi.rst
@@ -0,0 +1,3 @@
+- **Removed:** The option ``-I`` of coqchk was removed (it was
+ deprecated in Coq 8.8) (`#12613
+ <https://github.com/coq/coq/pull/12613>`_, by Gaëtan Gilbert).
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index af23747d43..4804822c99 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -436,7 +436,7 @@ let clear_hyps2 env sigma ids sign t cl =
with Evarutil.ClearDependencyError (id,err,inglobal) ->
error_replacing_dependency env sigma id err inglobal
-let internal_cut_gen ?(check=true) dir replace id t =
+let internal_cut ?(check=true) replace id t =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -457,23 +457,13 @@ let internal_cut_gen ?(check=true) dir replace id t =
Proofview.tclTHEN
(Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun sigma ->
- let (sigma,ev,ev') =
- if dir then
- let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
- let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
- (sigma,ev,ev')
- else
- let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
- let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
- (sigma,ev,ev') in
+ let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in
(sigma, term)
end)
end
-let internal_cut ?(check=true) = internal_cut_gen ~check true
-let internal_cut_rev ?(check=true) = internal_cut_gen ~check false
-
let assert_before_then_gen b naming t tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
@@ -500,7 +490,7 @@ let assert_after_then_gen ?err b naming t tac =
Proofview.Goal.enter begin fun gl ->
let id = find_name b (LocalAssum (make_annot Anonymous Sorts.Relevant,t)) naming gl in
Tacticals.New.tclTHENFIRST
- (replace_error_option err (internal_cut_rev b id t))
+ (replace_error_option err (internal_cut b id t <*> Proofview.cycle 1))
(tac id)
end
diff --git a/test-suite/ltac2/syntax.v b/test-suite/ltac2/syntax.v
new file mode 100644
index 0000000000..872b2142d0
--- /dev/null
+++ b/test-suite/ltac2/syntax.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Type ('a, 'b, 'c) t.
+Ltac2 Type ('a) u.
+Ltac2 Type 'a v.
+
+Ltac2 foo
+ (f : ('a, 'b, 'c) t -> ('a -> 'a, 'b -> 'c, 'c * 'c) t)
+ (x : ('a, 'b, 'c) t) :=
+ f x.
+
+Ltac2 bar (x : 'a u) (y : ('b) v) := x.
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 9097195721..0086516785 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -467,7 +467,7 @@ vok: $(VOFILES:%.vo=%.vok)
.PHONY: vok
validate: $(VOFILES)
- $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
+ $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^
.PHONY: validate
only: $(TGTS)
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 3af39ec59a..bec9632e84 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -262,12 +262,16 @@ GRAMMAR EXTEND Gram
| "1" LEFTA
[ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ]
| "0"
- [ "("; t = tac2type LEVEL "5"; ")" -> { t }
+ [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid ->
+ { match p, qid with
+ | [t], None -> t
+ | _, None -> CErrors.user_err ~loc (Pp.str "Syntax error")
+ | ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p)
+ }
| id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) }
| "_" -> { CAst.make ~loc @@ CTypVar Anonymous }
| qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) }
- | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
- { CAst.make ~loc @@ CTypRef (RelId qid, p) } ]
+ ]
];
locident:
[ [ id = Prim.ident -> { CAst.make ~loc id } ] ]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 13:28:28 +0000