From 5f53c5415d0bde33509eb53db7ef230819266420 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 18 Jun 2006 12:08:58 +0000 Subject: [PATCH] instead of including library_notation we include logic/equality that is smaller --- helm/software/components/binaries/tptp2grafite/main.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml index 51c7bbe48..871ff7b56 100644 --- a/helm/software/components/binaries/tptp2grafite/main.ml +++ b/helm/software/components/binaries/tptp2grafite/main.ml @@ -305,7 +305,7 @@ let _ = let extra_statements_start = [ GA.Executable(floc,GA.Command(floc, GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile))); - GA.Executable(floc,GA.Command(floc, GA.Include(floc,"library_notation.ma")))] + GA.Executable(floc,GA.Command(floc, GA.Include(floc,"logic/equality.ma")))] in List.iter pp extra_statements_start; List.iter -- 2.39.2