search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.85k stars 649 forks source link

Set Bullet Behavior and Require Import/Export #4491

Closed coqbot closed 8 years ago

coqbot commented 8 years ago

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4491 From: @robbertkrebbers Reported version: 8.5 CC: @gares

coqbot commented 8 years ago

Comment author: @robbertkrebbers

[Set Bullet Behavior "Strict Subproofs"] is only propagated by one level of require exporting, but not by two levels. For example:

File A.v: Require Export mathcomp.ssreflect.ssreflect. Global Set Bullet Behavior "Strict Subproofs".

File B1.v: ( Here we have checked bullets ) Require Export A. Goal True /\ True. split.

File B2.v: ( Here we do not have checked bullets ) Require Export B1. Goal True /\ True. split.

coqbot commented 8 years ago

Comment author: @gares

It might have something to do with the fact that the ml code of ssreflect (actually its initialization function) sets the bullets behavior to None).

It may be, just guessing, that this function is called late.

One can test if by commenting out a line in ssreflect.ml4 and put instead a Set in ssreflect.v (I'm on battery power now, I'm not doing it).

Best,

coqbot commented 8 years ago

Comment author: @robbertkrebbers

Created attachment 647 Move bullet initialization to ssreflect.v

Attached file: ssr_bullets.patch (text/plain, 2596 bytes) Description: Move bullet initialization to ssreflect.v

coqbot commented 8 years ago

Comment author: @robbertkrebbers

That seems to work. I have attached a patch. Thank you.

coqbot commented 8 years ago

Comment author: @gares

many thanks for the patch!

coqbot commented 8 years ago

Comment author: @gares

Fixed in ssreflect's git repo..