Subject: Ssreflect Users Discussion List
List archive
- From: Enrico Tassi <>
- To:
- Subject: Re: [ssreflect] Running computations inside Coq
- Date: Wed, 10 Feb 2016 08:54:35 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=None
- Ironport-phdr: 9a23:lm7AiRBTPiLtWmuZAyeSUyQJP3N1i/DPJgcQr6AfoPdwSP7+p8bcNUDSrc9gkEXOFd2CrakU1KyN6uu5ADBIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKbpotaKOlkArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kr8jV7FWCDktL0gw/9eutB/ZTALJ530GU2xQnAAbLRLC6UTXWI3wuSyyiuNmwyjSacDwV7E/XnK+5rxwSTfpjj0GPng36jeE2YRLkKtHrUf59FREyInObdTNOQ==
On Wed, Feb 10, 2016 at 08:38:04AM +0100, Ralf Jung wrote:
> > Definition master_key : unit := tt.
> > Global Opaque master_key.
>
> but I do not know if this has any undesired side-effects.
Unfortunately the opacity provided by "Opaque" is not as strong as the
one provided by "Qed". Opaque is a directive honoured by some Coq
tactics and it is just a hint to the kernel. The kernel would happily
unfold constants declared as Opaque, but would not unfold constants
that are Qed-opaque.
The point of locking constants is mostly to circumvent performance
issues in the kernel. Hence your solution would make the system
terribly slow (i.e. diverging).
Best,
--
Enrico Tassi
- [ssreflect] Running computations inside Coq, Felipe Cerqueira, 02/05/2016
- Re: [ssreflect] Running computations inside Coq, Emilio Jesús Gallego Arias, 02/06/2016
- Re: [ssreflect] Running computations inside Coq, Felipe Cerqueira, 02/06/2016
- Re: [ssreflect] Running computations inside Coq, Laurent Thery, 02/06/2016
- Re: [ssreflect] Running computations inside Coq, Ralf Jung, 02/10/2016
- Re: [ssreflect] Running computations inside Coq, Enrico Tassi, 02/10/2016
- Re: [ssreflect] Running computations inside Coq, Ralf Jung, 02/10/2016
- Re: [ssreflect] Running computations inside Coq, Emilio Jesús Gallego Arias, 02/06/2016
- Re: [ssreflect] Running computations inside Coq, Laurent Thery, 02/06/2016
- Re: [ssreflect] Running computations inside Coq, Felipe Cerqueira, 02/06/2016
- Re: [ssreflect] Running computations inside Coq, Emilio Jesús Gallego Arias, 02/06/2016
Archive powered by MHonArc 2.6.18.