Subject: Ssreflect Users Discussion List
List archive
[ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1801, characters 35-41: Assertion failed. Please report.
Chronological Thread
- From: Jason Gross <>
- To: ssreflect <>
- Subject: [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1801, characters 35-41: Assertion failed. Please report.
- Date: Thu, 12 Jun 2014 13:01:22 +0100
Is this mailing list the proper place to be reporting bugs in ssreflect?
Anyway,
Require Import Ssreflect.ssreflect.
Goal True.
do !match goal with _ => exact I end.
(* Toplevel input, characters 15-51:
Anomaly: File "tactics/tacinterp.ml", line 1801, characters 35-41: Assertion failed.
Please report. *)
ssr 1.4 on Coq 8.4pl4, I believe
-Jason
- [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1801, characters 35-41: Assertion failed. Please report., Jason Gross, 06/12/2014
Archive powered by MHonArc 2.6.18.