(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
(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))
GA.NSkip floc; GA.NMerge floc]))])
fv))
else [])@
- [GA.Executable(floc,GA.Command(floc, GA.NQed(floc)))]
+ [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+ GA.NSemicolon(floc)]))]@
+ [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
;;
let generate_tactics fv ueq_case =
(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))); ] @
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