]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
legacy development created
[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / Base / ext / preamble.ma
index b4c69f299f366435e7fbad576a9d2c8437580691..6a41598bbfd72c017d69cb3cfc17c4ba6e69a411 100644 (file)
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble".
 
-include' "legacy/coq.ma".
+include' "../../../../legacy/coq.ma".
 
 (* FG: This is because "and" is a reserved keyword of the parser *)
 alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".