From ef81020b09c01bd12a3d7083104d90f7edca6893 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Jun 2006 11:23:51 +0000 Subject: [PATCH] ... --- .../components/binaries/tptp2grafite/main.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml index 3c7d5f934..03f8f2e9f 100644 --- a/helm/software/components/binaries/tptp2grafite/main.ml +++ b/helm/software/components/binaries/tptp2grafite/main.ml @@ -306,9 +306,17 @@ let _ = GA.Executable(floc,GA.Command(floc, GA.Include(floc,"legacy/coq.ma")))] in List.iter pp extra_statements_start; - print_endline + List.iter + (fun (n,s) -> + print_endline (LexiconAstPp.pp_command (LA.Alias(floc, - LA.Ident_alias("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"))) ^ "."); + LA.Ident_alias(n,s))) ^ ".")) + [("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"); + ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con"); + ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con"); + ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con"); + ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con"); + ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")]; List.iter pp grafite_ast_statements; exit 0 -- 2.39.2