Exportar código de pruebas

Re: Exportar código de pruebas

de Leonardo Martin Piñeyro Rodriguez -
Número de respuestas: 0

En Mac la app corre en `/Applications`, entonces se ve que cuando le das un path relativo para la extracción lo va a intentar crear en `/Applications/Coq(...)` y no tiene permisos. Si ponés un path absoluto a una dirección donde Coq pueda escribir funciona bien, como por ejemplo:

`Extraction "/Users/<user>/Desktop/test.hs" ref_id.`

Saludos,