let disambiguate_term status_ref term =
let status = !status_ref in
- let (aliases, metasenv, cic, _) =
+ let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases)
~metasenv:(MatitaMisc.get_proof_metasenv status) term)
in
let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status_ref := status;
cic
let disambiguate_lazy_term status_ref term =
(fun context metasenv ugraph ->
let status = !status_ref in
- let (aliases, metasenv, cic, ugraph) =
+ let (diff, metasenv, cic, ugraph) =
singleton
(MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
~initial_ugraph:ugraph ~aliases:status.aliases
~universe:(Some status.multi_aliases) ~context ~metasenv term)
in
let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status_ref := status;
cic, metasenv, ugraph)
(* also adds them to the Db *)
CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
let status =
- List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
+ List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
status new_coercions in
let statement_of name =
GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
| GrafiteAst.Inductive _ -> assert false
| GrafiteAst.Theorem _ -> None in
- let (aliases, metasenv, cic, _) =
+ let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
| Intermediate _ -> assert false
in
let status = { status with proof_status = proof_status } in
- let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status, cic
let disambiguate_command status = function