From: Claudio Sacerdoti Coen Date: Fri, 8 May 2009 22:27:02 +0000 (+0000) Subject: Stupid typing error fixed. X-Git-Tag: make_still_working~4000 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a5126dcf31146ae630a38e7ca42a61d3eeadd0e6;p=helm.git Stupid typing error fixed. --- 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