+and proc_const st what =
+ let _, dtext = test_depth st in
+ let script = [T.Apply (what, dtext)] in
+ mk_intros st what script
+
and proc_appl st what hd tl =
let proceed, dtext = test_depth st in
let script = if proceed then
and proc_appl st what hd tl =
let proceed, dtext = test_depth st in
let script = if proceed then
| C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
| C.ARel _ as what -> proc_rel (f st) what
| C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
| C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
| C.ARel _ as what -> proc_rel (f st) what
| C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
| C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
| what -> proc_other (f st) what
| C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
| what -> proc_other (f st) what
List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars ||
List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars ||
List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars