From 52b441a5c783fff87fdac3e80b7f5c8d4c7fa7f7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 7 Sep 2006 15:15:16 +0000 Subject: [PATCH] Missing alias added. --- .../matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma index 5728f3ba6..6aea5b76b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma @@ -16,6 +16,9 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble". 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)". + (* FG/CSC: These aliases should disappear: we would like to write something * like: "disambiguate in cic:/Coq/*" *) -- 2.39.2