let intro = get_intro name in
proc_proof (add st entry intro) t
-and proc_letin st what name v t =
+and proc_letin st what name v w t =
let intro = get_intro name in
let proceed, dtext = test_depth st in
let script = if proceed then
in
st, C.Decl (H.cic ity), rqv
| None ->
- (*CSC: here we need the type of v *)
- st, C.Def (H.cic v, assert false), [T.LetIn (intro, v, dtext)]
+ st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)]
in
let entry = Some (name, hyp) in
let qt = proc_proof (next (add st entry intro)) t 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
{st with context = context; clears = clears; clears_note = note; }
in
match t with
- | C.ALambda (_, name, w, t) -> proc_lambda st name w t
- | C.ALetIn (_, name, v, ty, t) as what -> assert false (*proc_letin (f st) what name v 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.ALambda (_, name, w, t) -> proc_lambda st name w t
+ | 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
and proc_bkd_proofs st synth names classes ts =
try
(* 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