with
| Cic.MutInd (uri, tyno, _) ->
(GrafiteAst.Type (uri, tyno) :: types)
- | _ -> raise Disambiguate.NoWellTypedInterpretation)
+ | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]]))
in
let types = List.fold_left disambiguate [] types in
GrafiteAst.Decompose (loc, types, what, names)
let new_coercions =
CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
let status =
- List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
+ List.fold_left (fun s (uri,o,_) ->
+ let status = MatitaSync.add_obj uri o status in
+ {status with coercions = uri :: status.coercions})
status new_coercions in
+ let status = {status with coercions = coer_uri :: status.coercions} in
let statement_of name =
GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
(CicNotationPt.Ident (name, None)))
proof_status = No_proof;
options = default_options ();
objects = [];
+ coercions = [];
notation_ids = [];
}