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
aux ty
in
let ty_src,ty_tgt = extract_last_two_p coer_ty in
- let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in
- let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in
+ let context = [] in
+ let src_uri =
+ let ty_src = CicReduction.whd context ty_src in
+ UriManager.uri_of_string (CicUtil.uri_of_term ty_src)
+ in
+ let tgt_uri =
+ let ty_tgt = CicReduction.whd context ty_tgt in
+ UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt)
+ in
let new_coercions =
(* also adds them to the Db *)
CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
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
CicUnification.fo_unif metasenv [] body_type ty ugraph
in
if metasenv <> [] then
- command_error
- "metasenv not empty while giving a definition with body";
+ command_error (
+ "metasenv not empty while giving a definition with body: " ^
+ CicMetaSubst.ppmetasenv metasenv []) ;
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 status, cmd = disambiguate_command status cmd in
status, (TacticAst.Command (loc, cmd))
| TacticAst.Macro (_, mac) ->
- command_error
- (sprintf ("The engine is not allowed to disambiguate any macro, "^^
- "in particular %s") (TacticAstPp.pp_macro_ast mac))
+ command_error (sprintf "The macro %s can't be in a script"
+ (TacticAstPp.pp_macro_ast mac))
let disambiguate_comment status c =
match c with