type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of (uri,arity, saturations) =
+let coercion_moo_statement_of (uri,arity, saturations,_) =
GrafiteAst.Coercion
(HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
saturations (GrafiteTypes.get_baseuri status)
in
let moo_content =
- List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
+ List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds)
in
let status = GrafiteTypes.add_moo_content moo_content status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
- List.map (fun u,_,_ -> u) compounds
+ List.map (fun u,_,_,_ -> u) compounds
module MatitaStatus =
struct
in
let is_a_coercion, arity_coercion = is_a_coercion uri in
if is_a_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_coercion,0))
+ Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0))
else if is_a_wanted_coercion then
- Some (uri, coercion_moo_statement_of (uri,arity_wanted,0))
+ Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0))
else
None)
lemmas)