From a39d9579cb2a227a49d23ae68d4f61f5d24b65f7 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Wed, 6 Dec 2000 21:10:01 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1079 85f007b7-540e-0410-9357-904b9bb8a0f7 --- PROBLEMES | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/PROBLEMES b/PROBLEMES index 2e72d63765..aed1579124 100644 --- a/PROBLEMES +++ b/PROBLEMES @@ -92,3 +92,13 @@ Montevideo/CtlTctl OK Montevideo/RailroadCrossing File "./railroad_crossing.v", line 613, characters 2-20 Anomaly: useInversionLemma. Please report. + +Nijmegen OK +Utrecht/Ramsey OK + +Utrecht/ABP +coqc -q -I . abp_base +File "./abp_base.v", line 42, characters 0-154 +Error: Cannot declare a variable or hypothesis over the term Y +because this term is not a type. + -- cgit v1.2.3