Skip to Content.
Sympa Menu

ssreflect - RE: [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1803, characters 35-41: Assertion failed. Please report.

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
Sent: 18 August 2014 17:04
To: ssreflect
Subject: [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1803, characters 35-41: Assertion failed. Please report.

 

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




Archive powered by MHonArc 2.6.18.

Top of Page