*)
let get_type msg st bo =
try
- let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
+ let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
ty
with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
let get_ind_names uri tno =
try
- let ts = match E.get_obj Un.empty_ugraph uri with
+ let ts = match E.get_obj Un.oblivion_ugraph uri with
| C.InductiveDefinition (ts, _, _, _), _ -> ts
| _ -> assert false
in
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