aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli2
-rw-r--r--COMPATIBILITY4
-rw-r--r--dev/build/windows/makecoq_mingw.sh4
-rw-r--r--dev/ci/appveyor.bat14
-rw-r--r--doc/refman/RefMan-ltac.tex9
-rw-r--r--intf/vernacexpr.ml3
-rw-r--r--parsing/g_proofs.ml46
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--printing/ppvernac.ml5
-rw-r--r--stm/asyncTaskQueue.ml4
-rw-r--r--stm/stm.ml5
-rwxr-xr-xtest-suite/coq-makefile/template/init.sh1
-rw-r--r--test-suite/success/qed_export.v18
-rw-r--r--vernac/lemmas.ml17
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/vernacentries.ml2
16 files changed, 41 insertions, 63 deletions
diff --git a/API/API.mli b/API/API.mli
index 536efea78..3ed326ff0 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3670,7 +3670,7 @@ sig
type lname = Names.Name.t Loc.located
type lident = Names.Id.t Loc.located
type opacity_flag =
- | Opaque of lident list option
+ | Opaque
| Transparent
type locality_flag = bool
type inductive_kind =
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 78dfabaa3..b5fed7f01 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -5,6 +5,10 @@ Potential sources of incompatibilities between Coq V8.6 and V8.7
error rather than a warning when the superfluous name is already in
use. The easy fix is to remove the superfluous name.
+- Proofs ending in "Qed exporting ident, .., ident" are not supported
+ anymore. Constants generated during `abstract` are kept private to the
+ local environment.
+
Potential sources of incompatibilities between Coq V8.5 and V8.6
----------------------------------------------------------------
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index f3e4cec0b..f12cbe0a7 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -910,6 +910,10 @@ function make_camlp5 {
log2 make install
# For some reason gramlib.a is not copied, but it is required by Coq
cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/"
+ # For some reason META is not copied, but it is required by coq_makefile
+ log2 make -C etc META
+ mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/"
+ cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/"
log2 make clean
build_post
fi
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index ca6a5643c..e2fbf1f6d 100644
--- a/dev/ci/appveyor.bat
+++ b/dev/ci/appveyor.bat
@@ -23,13 +23,19 @@ if %USEOPAM% == false (
call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
-destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
- -setup %CYGROOT%\%SETUP%
- copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis
- 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\*
+ -setup %CYGROOT%\%SETUP% || GOTO ErrorExit
+ copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
+ 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
)
if %USEOPAM% == true (
%CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
-P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
- %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh
+ %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit
)
+
+GOTO :EOF
+
+:ErrorExit
+ ECHO ERROR MakeCoq_MinGW.bat failed
+ EXIT /b 1
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c8e2ae2dd..574591185 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1106,19 +1106,14 @@ Fail all:let n:= numgoals in guard n=2.
Reset Initial.
\end{coq_eval}
-\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}\comindex{Qed exporting}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}
\index{Tacticals!abstract@{\tt abstract}}\index{Tacticals!transparent\_abstract@{\tt transparent\_abstract}}}
From the outside ``\texttt{abstract \tacexpr}'' is the same as
{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
current goal and \textit{n} is chosen so that this is a fresh name.
-Such auxiliary lemma is inlined in the final proof term
-unless the proof is ended with ``\texttt{Qed exporting}''. In such
-case the lemma is preserved. The syntax
-``\texttt{Qed exporting }\ident$_1$\texttt{, ..., }\ident$_n$''
-is also supported. In such case the system checks that the names given by the
-user actually exist when the proof is ended.
+Such an auxiliary lemma is inlined in the final proof term.
This tactical is useful with tactics such as \texttt{omega} or
\texttt{discriminate} that generate huge proof terms. With that tool
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index cfc3343b6..03e8ea43d 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -139,8 +139,7 @@ type search_restriction =
type rec_flag = bool (* true = Rec; false = NoRec *)
type verbose_flag = bool (* true = Verbose; false = Silent *)
- (* list of idents for qed exporting *)
-type opacity_flag = Opaque of lident list option | Transparent
+type opacity_flag = Opaque | Transparent
type coercion_flag = bool (* true = AddCoercion false = NoCoercion *)
type instance_flag = bool option
(* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 42b5bfa93..e2c87bbbf 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -45,11 +45,9 @@ GEXTEND Gram
| IDENT "Existential"; n = natural; c = constr_body ->
VernacSolveExistential (n,c)
| IDENT "Admitted" -> VernacEndProof Admitted
- | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
- | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," ->
- VernacEndProof (Proved (Opaque (Some l),None))
+ | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None))
| IDENT "Save"; id = identref ->
- VernacEndProof (Proved (Opaque None, Some id))
+ VernacEndProof (Proved (Opaque, Some id))
| IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
| IDENT "Defined"; id=identref ->
VernacEndProof (Proved (Transparent,Some id))
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6fcfec80d..74c454334 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1292,8 +1292,8 @@ let build_new_goal_type () =
let is_opaque_constant c =
let cb = Global.lookup_constant c in
match cb.Declarations.const_body with
- | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None
- | Declarations.Undef _ -> Vernacexpr.Opaque None
+ | Declarations.OpaqueDef _ -> Vernacexpr.Opaque
+ | Declarations.Undef _ -> Vernacexpr.Opaque
| Declarations.Def _ -> Vernacexpr.Transparent
let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f371fb08c..10dd42ea9 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -718,10 +718,7 @@ open Decl_kinds
match o with
| None -> (match opac with
| Transparent -> keyword "Defined"
- | Opaque None -> keyword "Qed"
- | Opaque (Some l) ->
- keyword "Qed" ++ spc() ++ str"export" ++
- prlist_with_sep (fun () -> str", ") pr_lident l)
+ | Opaque -> keyword "Qed")
| Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
)
| VernacExactProof c ->
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 31ede2d8b..5d9b595d3 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -237,7 +237,7 @@ module Make(T : Task) = struct
type queue = {
active : Pool.pool;
queue : (T.task * expiration) TQueue.t;
- cleaner : Thread.t;
+ cleaner : Thread.t option;
}
let create size =
@@ -250,7 +250,7 @@ module Make(T : Task) = struct
{
active = Pool.create queue ~size;
queue;
- cleaner = Thread.create cleaner queue;
+ cleaner = if size > 0 then Some (Thread.create cleaner queue) else None;
}
let destroy { active; queue } =
diff --git a/stm/stm.ml b/stm/stm.ml
index e0064df9b..75ec946f0 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1385,7 +1385,7 @@ end = struct (* {{{ *)
stm_vernac_interp stop
~proof:(pobject, terminator)
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = (VernacEndProof (Proved (Opaque None,None))) }) in
+ expr = (VernacEndProof (Proved (Opaque,None))) }) in
ignore(Future.join checked_proof);
end;
RespBuiltProof(proof,time)
@@ -1525,7 +1525,7 @@ end = struct (* {{{ *)
Reach.known_state ~cache:`No start;
stm_vernac_interp stop ~proof
{ verbose = false; loc; indentation = 0; strlen = 0;
- expr = (VernacEndProof (Proved (Opaque None,None))) };
+ expr = (VernacEndProof (Proved (Opaque,None))) };
`OK proof
end
with e ->
@@ -1976,7 +1976,6 @@ let collect_proof keep cur hd brkind id =
| id :: _ -> Names.Id.to_string id in
let loc = (snd cur).loc in
let rec is_defined_expr = function
- | VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) -> true
| VernacTime (_, e) -> is_defined_expr e
| VernacRedirect (_, (_, e)) -> is_defined_expr e
| VernacTimeout (_, e) -> is_defined_expr e
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index 803fe8029..c4bd11c57 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -2,6 +2,7 @@ set -e
set -o pipefail
export PATH=$COQBIN:$PATH
+export LC_ALL=C
rm -rf theories src Makefile Makefile.conf tmp
git clean -dfx || true
diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
deleted file mode 100644
index b3e41ab1f..000000000
--- a/test-suite/success/qed_export.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Lemma a : True.
-Proof.
-assert True as H.
- abstract (trivial) using exported_seff.
-exact H.
-Fail Qed exporting a_subproof.
-Qed exporting exported_seff.
-Check ( exported_seff : True ).
-
-Lemma b : True.
-Proof.
-assert True as H.
- abstract (trivial) using exported_seff2.
-exact H.
-Qed.
-
-Fail Check ( exported_seff2 : True ).
-
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2b97437e6..2c8f6ec9d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -310,12 +310,6 @@ let get_proof proof do_guard hook opacity =
in
id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-let check_exist =
- List.iter (fun (loc,id) ->
- if not (Nametab.exists_cci (Lib.make_path id)) then
- user_err ?loc (pr_id id ++ str " does not exist.")
- )
-
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
@@ -323,17 +317,16 @@ let universe_proof_terminator compute_guard hook =
admit (id,k,pe) pl (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
- let is_opaque, export_seff, exports = match opaque with
- | Vernacexpr.Transparent -> false, true, []
- | Vernacexpr.Opaque None -> true, false, []
- | Vernacexpr.Opaque (Some l) -> true, true, l in
+ let is_opaque, export_seff = match opaque with
+ | Vernacexpr.Transparent -> false, true
+ | Vernacexpr.Opaque -> true, false
+ in
let proof = get_proof proof compute_guard
(hook (Some (fst proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some (_,id) -> save_anonymous ~export_seff proof id
- end;
- check_exist exports
+ end
end
let standard_proof_terminator compute_guard hook =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 89b18d254..81218308f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -846,9 +846,9 @@ let obligation_terminator name num guard hook auto pf =
let obl = obls.(num) in
let status =
match obl.obl_status, opq with
- | (_, Evar_kinds.Expand), Vernacexpr.Opaque _ -> err_not_transp ()
- | (true, _), Vernacexpr.Opaque _ -> err_not_transp ()
- | (false, _), Vernacexpr.Opaque _ -> Evar_kinds.Define true
+ | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
+ | (true, _), Vernacexpr.Opaque -> err_not_transp ()
+ | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
| (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
| (_, status), Vernacexpr.Transparent -> status
in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0c7599450..83296cf58 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -507,7 +507,7 @@ let vernac_exact_proof c =
(* spiwack: for simplicity I do not enforce that "Proof proof_term" is
called only at the begining of a proof. *)
let status = Pfedit.by (Tactics.exact_proof c) in
- save_proof (Vernacexpr.(Proved(Opaque None,None)));
+ save_proof (Vernacexpr.(Proved(Opaque,None)));
if not status then Feedback.feedback Feedback.AddedAxiom
let vernac_assumption locality poly (local, kind) l nl =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 21:34:23 +0000