From a5126dcf31146ae630a38e7ca42a61d3eeadd0e6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 May 2009 22:27:02 +0000 Subject: [PATCH] Stupid typing error fixed. --- helm/software/matita/tests/ng_commands.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma index 755921938..cbb73844d 100644 --- a/helm/software/matita/tests/ng_commands.ma +++ b/helm/software/matita/tests/ng_commands.ma @@ -56,5 +56,5 @@ and nmzero (m:mat 0 (dt ?)) : nnat 0 (dt ?) ≝ match m return ? with [ mS n ⇒ nnzero n ]. -nrecord pair (n: nat) (x: dt n) (label: Type): Type ≝ - { lbl:label; l: pair label; r: pair label}. \ No newline at end of file +nrecord pair (n: nat) (x: DT n) (label: Type): Type ≝ + { lbl:label; l: pair n x label; r: pair n x label}. \ No newline at end of file -- 2.39.2