From 1e341b177cc490278c4b9561f7ba3eeb41a1ab0f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 9 Jun 2005 16:08:57 +0000 Subject: [PATCH] No more explicit types for the branches of the matches: all the bugs preventing automatic type inference have been fixed. --- helm/matita/tests/match.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma index 3dbb580d5..c75d4fda8 100644 --- a/helm/matita/tests/match.ma +++ b/helm/matita/tests/match.ma @@ -164,7 +164,7 @@ let rec minus n m \def match n with [ O \Rightarrow O | (S p) \Rightarrow - [\lambda n:nat.nat] match m with + match m with [O \Rightarrow (S p) | (S q) \Rightarrow minus p q ]]. @@ -280,7 +280,7 @@ let rec leb n m \def match n with [ O \Rightarrow true | (S p) \Rightarrow - [\lambda n:nat.bool] match m with + match m with [ O \Rightarrow false | (S q) \Rightarrow leb p q]]. -- 2.39.2