decentralizing core notation

[helm.git] / matita / matita / lib / arithmetics / factorial.ma

diff --git a/matita/matita/lib/arithmetics/factorial.ma b/matita/matita/lib/arithmetics/factorial.ma
index fc2320a948cbd324ddfe900db2af3f33837866f7..60519e9829f185f0b614b46923f346156a1ec911 100644 (file)
--- a/matita/matita/lib/arithmetics/factorial.ma
+++ b/matita/matita/lib/arithmetics/factorial.ma
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/exp.ma".
+include "basics/core_notation/fact_1.ma".
 
 let rec fact n ≝
   match n with