aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorPierre Roux2020-04-11 14:03:54 +0200
committerPierre Roux2020-05-22 12:15:22 +0200
commitf44ec99f9ae9b8aa8d77c39795dd4de2a5724218 (patch)
tree79773cecfa12b8526d0162d5ed62269b8a312058 /test-suite
parentfff80866a5a61d8d53e34a1afdbe6475dc6ea5d9 (diff)
[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.
Diffstat (limited to 'test-suite')
0 files changed, 0 insertions, 0 deletions