]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/pts_dummy_new/subterms.ma
- pts_dummy/pts_dummy_new: non compiling parts commented out
[helm.git] / matita / matita / lib / pts_dummy_new / subterms.ma
index 86a8507ed55bb13590988bd76476056a3354f124..bc7fa2a057ba0cbc612b241eb59b8d9cbb18c74e 100644 (file)
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/subst.ma".
+include "pts_dummy_new/subst.ma".
 
 inductive subterm : T → T → Prop ≝
   | appl : ∀M,N. subterm M (App M N)