From 3030cb87adf2b652bd5d6c21be25ab246549c573 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 Jul 2005 08:59:17 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 9a53f4cc6..d1f44f3e6 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,6 +2,10 @@ (**********************************************************************) TODO +- Bug: non disambigua + inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false). + perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug + stupido da qualche parte - preoccupante: per inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false). noi generiamo anche i_rec e i_rect che Coq non genera (e che NON dovrebbero -- 2.39.2