From 15b42d9cdb401538a9ba8d9ab82d2ad046596e8b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 30 May 2006 09:19:14 +0000 Subject: [PATCH] A -> Univ --- helm/software/components/binaries/tptp2grafite/main.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml index 4a5781243..4042d92d1 100644 --- a/helm/software/components/binaries/tptp2grafite/main.ml +++ b/helm/software/components/binaries/tptp2grafite/main.ml @@ -4,6 +4,8 @@ module PT = CicNotationPt;; module A = Ast;; let floc = HExtlib.dummy_floc;; +let universe = "Univ" ;; + let kw = [ "and","myand" ];; @@ -85,7 +87,7 @@ let build_ctx_for_arities univesally arities t = | (name,nargs)::tl -> PT.Binder (binder, - (mk_ident name,Some (mk_arrow "A" nargs)), + (mk_ident name,Some (mk_arrow universe nargs)), aux tl) in aux arities @@ -101,7 +103,7 @@ let convert_atom universally a = | A.False -> mk_ident "False" | A.Eq (l,r) | A.NotEq (l,r) -> (* removes the negation *) - PT.Appl [mk_ident "eq";mk_ident "A";convert_term l;convert_term r] + PT.Appl [mk_ident "eq";mk_ident universe;convert_term l;convert_term r] in build_ctx_for_arities universally (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a) @@ -180,7 +182,7 @@ let convert_ast statements context = function let f = PT.Binder (`Forall, - (mk_ident "A",Some (PT.Sort `Set)), + (mk_ident universe,Some (PT.Sort `Set)), convert_formula fv false context f) in let o = PT.Theorem (`Theorem,name,f,None) in -- 2.39.2