fixed bug in coercion application, input/output swapped in unification

[helm.git] / helm / software / components / tptp_grafite / tptp2grafite.ml

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 244cd1d728975ebc22f000402bf99e5e589329ea..c63fca74166bfc137203a91e4033d90040a6c4db 100644 (file)
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -354,7 +354,7 @@ let convert_ast ng statements context = function
                (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))), 
                convert_formula fv false context f)
           in
-          let o = PT.Theorem (`Theorem,name,f,None) in
+          let o = PT.Theorem (`Theorem,name,f,None,`Regular) in
           (statements @ 
           [ GA.Executable(floc,GA.Command(floc,
              (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @