PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
| TacticAst.Intros (_, Some num, names) ->
(* TODO Zack implement intros length *)
PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
| TacticAst.Intros (_, Some num, names) ->
(* TODO Zack implement intros length *)
| TacticAst.Reflexivity _ -> Tactics.reflexivity
| TacticAst.Assumption _ -> Tactics.assumption
| TacticAst.Contradiction _ -> Tactics.contradiction
| 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
UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
in
let metasenv = MatitaMisc.get_proof_metasenv status in
let (body_type, ugraph) =
CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
in
let (body_type, ugraph) =
CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
in
let body = CicMetaSubst.apply_subst subst body in
let ty = CicMetaSubst.apply_subst subst ty in
let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
let body = CicMetaSubst.apply_subst subst body in
let ty = CicMetaSubst.apply_subst subst ty in
let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in