let script = [T.Apply (what, dtext)] in
mk_intros st what script
+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
| 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.AConst _ as what -> proc_const (f st) what
| C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
| what -> proc_other (f st) what
(* object costruction *******************************************************)
-let is_theorem pars =
+let is_theorem pars =
+ pars = [] ||
List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars ||
List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars