Subject: Ssreflect Users Discussion List
List archive
RE: [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1803, characters 35-41: Assertion failed. Please report.
Chronological Thread
- From: Georges Gonthier <>
- To: Jason Gross <>, ssreflect <>
- Subject: RE: [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1803, characters 35-41: Assertion failed. Please report.
- Date: Mon, 18 Aug 2014 16:24:51 +0000
- Accept-language: en-GB, en-US
- Authentication-results: spf=pass (sender IP is 131.107.125.37) ;
Replacing the match with (fail || match …) makes the problem go away, so this looks more like an Ltac internal bug. (Also, the problem occurs with any other ssr tactical, such as do [..]). -- Georges
From: [mailto:]
On Behalf Of Jason Gross
Hi,
Here is some code that gives the anomaly. Replacing "first foo" with "[ foo | .. ]" makes it go away, which makes me think this is an ssr bug.
Ltac foo := idtac; try (idtac; let e := fresh "e" in match False with | True => idtac end; first foo). Goal True. foo.
I'm using ssr 1.4, Coq 8.4pl4.
-Jason |
- [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1803, characters 35-41: Assertion failed. Please report., Jason Gross, 08/18/2014
- RE: [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1803, characters 35-41: Assertion failed. Please report., Georges Gonthier, 08/18/2014
Archive powered by MHonArc 2.6.18.