(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))
else [])@
[GA.Executable(floc,GA.NTactic(floc, [
if (*ueq_case*) true then
- GA.NAuto (floc,(
+ GA.NAuto (floc,(Some
HExtlib.list_mapi
(fun _ i ->
mk_ident ("H" ^ string_of_int i))
context
,[]))
else
- GA.NAuto (floc,([],[
+ GA.NAuto (floc,(None,[
"depth",string_of_int 5;
"width",string_of_int 5;
"size",string_of_int 20;
else [])@
[GA.Executable(floc,GA.Tactic(floc, Some (
if true (*ueq_case*) then
- GA.AutoBatch (floc,([],["paramodulation","";
+ GA.AutoBatch (floc,(None,["paramodulation","";
"timeout",string_of_int !paramod_timeout]))
else
- GA.AutoBatch (floc,([],[
+ GA.AutoBatch (floc,(None,[
"depth",string_of_int 5;
"width",string_of_int 5;
"size",string_of_int 20;
(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))); ] @