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
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