coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Extraction and error reporting

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Extraction and error reporting
Date: Sat, 7 May 2011 01:47:47 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=sI8x+HTFtrb9VmuMHveuGy0xeejUgGfZBpVE+yKR82LHo8BnXgHOA6Nsl2P+egWnXz DrK6DfLJQGKpAl7bsti3OP1GxONbaL9asHM5V59JE9cdLP+9KPu4jx2krNNbCu0RQ6IS kLKWhE+1sdpLVZ3bYBQxu0YLjoYiSLTncAxIA=

Dear list

I'm trying report some errors in my code by adding things like

Parameter error_badly_masked: unit -> unit.
Extract Constant error_badly_masked => "Errors.error_badly_masked".

Definition .....
let tt := error_badly_masked tt in
....

But the extraction removes this call

Is it possible to forbid the extraction to remove call to parameters?

Thanks in advance

Alexandre

[Coq-Club] Extraction and error reporting, Alexandre Pilkiewicz
- Re: [Coq-Club] Extraction and error reporting, Francesco Zappa Nardelli
- Re: [Coq-Club] Extraction and error reporting, AUGER Cedric
  - [Coq-Club] Re: Extraction and error reporting, Alexandre Pilkiewicz
  - Re: [Coq-Club] Extraction and error reporting, AUGER Cedric