Equality has one right parameter and thus it's elimination principle has two

[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 ca0534c52b7f3ae410376808cdf63ac9ca4a8dec..c63fca74166bfc137203a91e4033d90040a6c4db 100644 (file)
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -221,7 +221,8 @@ let ng_generate_tactics fv ueq_case context arities =
   (HExtlib.list_mapi
    (fun (name,_) _-> 
      GA.Executable(floc,GA.NTactic(floc, 
-      [GA.NIntro (floc,name);GA.NDot(floc)])))
+      [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
+       GA.NDot(floc)])))
    arities)
   @
   (HExtlib.list_mapi
@@ -236,8 +237,9 @@ let ng_generate_tactics fv ueq_case context arities =
       (fun _ -> 
         [GA.Executable(floc,GA.NTactic(floc, 
           [GA.NApply (floc,
-            PT.Appl [mk_ident "ex_intro";PT.Implicit;PT.Implicit;
-              PT.Implicit;PT.Implicit]);GA.NBranch floc]));
+            PT.Appl
+             [mk_ident "ex_intro";PT.Implicit `JustOne;PT.Implicit `JustOne;
+              PT.Implicit `JustOne;PT.Implicit `JustOne]);GA.NBranch floc]));
          GA.Executable(floc,GA.NTactic(floc, 
           [GA.NPos (floc,[2])]))])
       fv)) 
@@ -272,6 +274,8 @@ let ng_generate_tactics fv ueq_case context arities =
                GA.NSkip floc; GA.NMerge floc]))])
       fv)) 
  else [])@
+    [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+                                        GA.NSemicolon(floc)]))]@
   [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
 ;;
 
@@ -350,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))); ] @
@@ -437,8 +441,9 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam
   let preamble = 
     match raw_preamble with
     | None -> 
-       pp (GA.Executable(floc,
-           GA.Command(floc,GA.Include(floc,true,"logic/equality.ma"))))
+      pp
+       (GA.Executable(floc,
+         GA.Command(floc,GA.Include(floc,true,`OldAndNew,"logic/equality.ma"))))
     | Some s -> s buri
   in
   let extra_statements_end = [] in