PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
| TacticAst.Intros (_, Some num, names) ->
(* TODO Zack implement intros length *)
- PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
+ PrimitiveTactics.intros_tac ~howmany:num
+ ~mk_fresh_name_callback:(namer_of names) ()
| TacticAst.Reflexivity _ -> Tactics.reflexivity
| TacticAst.Assumption _ -> Tactics.assumption
| TacticAst.Contradiction _ -> Tactics.contradiction
UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
in
let metasenv = MatitaMisc.get_proof_metasenv status in
- debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body);
let (body_type, ugraph) =
CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
in