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