Subject: Ssreflect Users Discussion List
List archive
- From: Frédéric Chyzak <>
- To:
- Subject: case: returns blank error message
- Date: Wed, 23 Oct 2013 09:11:54 +0200
- Organization: INRIA
Hi,
Maybe I am in a special case of case: (applied to equalities), but I would expect a more informative error message.
Frédéric
$ coq/bin/coqtop -I coqfinitgroup
Welcome to Coq 8.4pl2 (June 2013)
Coq < Require Import ssreflect.
Small Scale Reflection version 1.4 loaded.
Copyright 2005-2012 Microsoft Corporation and INRIA.
Distributed under the terms of the CeCILL-B license.
[Loading ML file ssreflect.cmxs ... done]
Coq < Lemma foo (e1 e2 : false = false) : e1 = e2.
1 subgoal
e1 : false = false
e2 : false = false
============================
e1 = e2
foo < case: e1.
Toplevel input, characters 0-8:
> case: e1.
> ^^^^^^^^
Error:
foo <
- case: returns blank error message, Frédéric Chyzak, 10/23/2013
- Re: case: returns blank error message, Benjamin Werner, 10/23/2013
- RE: case: returns blank error message, Georges Gonthier, 10/23/2013
- Re: case: returns blank error message, Frédéric Chyzak, 10/23/2013
- Re: case: returns blank error message, Bas Spitters, 10/25/2013
- Re: case: returns blank error message, Benjamin Werner, 10/23/2013
Archive powered by MHonArc 2.6.18.