type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of arity uri =
+let coercion_moo_statement_of (uri,arity) =
GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity)
let refinement_toolkit = {
baseuri
in
let moo_content =
- List.map (coercion_moo_statement_of arity) (uri::compounds)
+ List.map coercion_moo_statement_of ((uri,arity)::compounds)
in
let status = GrafiteTypes.add_moo_content moo_content status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
- compounds
+ List.map fst compounds
let eval_tactical ~disambiguate_tactic status tac =
let apply_tactic = apply_tactic ~disambiguate_tactic in
in
let is_a_coercion, arity_coercion = is_a_coercion uri in
if is_a_coercion then
- Some (uri, coercion_moo_statement_of arity_coercion uri)
+ Some (uri, coercion_moo_statement_of (uri,arity_coercion))
else if is_a_wanted_coercion then
- Some (uri, coercion_moo_statement_of arity_wanted uri)
+ Some (uri, coercion_moo_statement_of (uri,arity_wanted))
else
None)
lemmas)
let status, lemmas = add_obj uri obj status in
{status with
GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+ (*CSC: I throw away the arities *)
uri::lemmas
| GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) ->
Setoids.add_relation id a aeq refl sym trans;