From f44ec99f9ae9b8aa8d77c39795dd4de2a5724218 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 11 Apr 2020 14:03:54 +0200 Subject: [coqchk] Fix #5030 When encountering ```Coq Module M : T. ... Lemma c :... ... Qed. ... End M. ``` every field `c` without body in `T` but with a body in `M` is registered as opacified in a table along with all constants `opacified(c)` without body in the environment at this point (i.e., all axioms potentially used by c). Then, when printing axioms, if `c` appears in the final environment it is replaced by `opacified(c)` in the resulting list of axioms. --- doc/changelog/08-tools/12076-fix-5030.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/08-tools/12076-fix-5030.rst (limited to 'doc') diff --git a/doc/changelog/08-tools/12076-fix-5030.rst b/doc/changelog/08-tools/12076-fix-5030.rst new file mode 100644 index 0000000000..afb59b1cde --- /dev/null +++ b/doc/changelog/08-tools/12076-fix-5030.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Fix #5030 (coqchk reports names from opaque modules as axioms) + (`#12076 `_, + by Pierre Roux). -- cgit v1.2.3