in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as

[helm.git] / helm / software / matita / tests / ng_tactics.ma

diff --git a/helm/software/matita/tests/ng_tactics.ma b/helm/software/matita/tests/ng_tactics.ma
index 6c7e161f68d6ea8692024d874e9f697ffdd057a1..3bb4a6fa4c8b3e3fd5ebe176546b1bd0d23f2f23 100644 (file)
--- a/helm/software/matita/tests/ng_tactics.ma
+++ b/helm/software/matita/tests/ng_tactics.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ng_pts.ma".
 include "nat/plus.ma".
 
 ntheorem test1 : ∀n:nat.n = S n + n → S n = (S (S n)).