(* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term
| GrafiteAst.ApplyS (_, term, params) ->
Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
let coercion_moo_statement_of (uri,arity, saturations) =
- GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity, saturations)
+ GrafiteAst.Coercion
+ (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
let refinement_toolkit = {
RefinementTool.type_of_aux' =
}
let eval_coercion status ~add_composites uri arity saturations =
+ let uri =
+ try CicUtil.uri_of_term uri
+ with Invalid_argument _ ->
+ raise (Invalid_argument "coercion can only be constants/constructors")
+ in
let status,compounds =
GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
saturations (GrafiteTypes.get_baseuri status)