(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))
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