(** perform debugging output? *)
let debug = false
+let debug_print = fun _ -> ()
(** debugging print *)
let warn s =
if debug then
- prerr_endline ("DECOMPOSE: " ^ s)
+ debug_print ("DECOMPOSE: " ^ s)
let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let old_context_len = List.length context in
- let termty = CicTypeChecker.type_of_aux' metasenv context term in
-
- let rec make_list termty =
+ let termty,_ =
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let rec make_list termty =
(* N.B.: altamente inefficente? *)
let rec search_inductive_types urilist termty =
(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *)
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let old_context_len = List.length context in
- let termty = CicTypeChecker.type_of_aux' metasenv context term' in
+ let termty,_ =
+ CicTypeChecker.type_of_aux' metasenv context term'
+ CicUniv.empty_ugraph in
warn ("elim_clear termty= " ^ CicPp.ppterm termty);
match termty with
C.MutInd (uri,typeno,exp_named_subst)
(T.then_
~start:(
if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *)
- then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end
- else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
+ then begin debug_print ("%%%%%%% no clear"); T.id_tac end
+ else begin debug_print ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end)
~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)))
status
)))