let context =
match context with
| Some c -> c
- | None -> MatitaMisc.get_proof_context status goal
+ | None -> MatitaTypes.get_proof_context status goal
in
let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases)
- ~context ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
+ ~context ~metasenv:(MatitaTypes.get_proof_metasenv status) term)
in
let status = MatitaTypes.set_metasenv metasenv status in
let status = MatitaSync.set_proof_aliases status diff in
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 apply_tactic tactic (status, goal) =
(* prerr_endline "apply_tactic"; *)
-(* prerr_endline (Continuationals.Stack.pp (MatitaMisc.get_stack status)); *)
- let starting_metasenv = MatitaMisc.get_proof_metasenv status in
+(* prerr_endline (Continuationals.Stack.pp (MatitaTypes.get_stack status)); *)
+ let starting_metasenv = MatitaTypes.get_proof_metasenv status in
let before = List.map (fun g, _, _ -> g) starting_metasenv in
(* prerr_endline "disambiguate"; *)
let status_ref, tactic = disambiguate_tactic status goal tactic in
- let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in
- let proof = MatitaMisc.get_current_proof !status_ref in
+ let metasenv_after_refinement = MatitaTypes.get_proof_metasenv !status_ref in
+ let proof = MatitaTypes.get_current_proof !status_ref in
let proof_status = proof, goal in
let needs_reordering, always_opens_a_goal = classify_tactic tactic in
let tactic = tactic_of_ast tactic in
let apply_tactic tac = tac
let goals (_, opened, closed) = opened, closed
let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
- let get_stack (status, _) = MatitaMisc.get_stack status
+ let get_stack (status, _) = MatitaTypes.get_stack status
let set_stack stack (status, opened, closed) =
- MatitaMisc.set_stack stack status, opened, closed
+ MatitaTypes.set_stack stack status, opened, closed
let inject (status, _) = (status, [], [])
let focus goal (status, _, _) = (status, goal)
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)))
match obj with
GrafiteAst.Inductive (_,(name,_,_,_)::_)
| GrafiteAst.Record (_,name,_,_) ->
- Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
+ Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind"))
| GrafiteAst.Inductive _ -> assert false
| GrafiteAst.Theorem _ -> None in
let (diff, metasenv, cic, _) =
add_moo_content [cmd] status
| GrafiteAst.Include (loc, path) ->
let absolute_path = make_absolute opts.include_paths path in
- let moopath = MatitaMisc.obj_file_of_script absolute_path in
+ let moopath = MatitacleanLib.obj_file_of_script absolute_path in
let status = ref status in
if not (Sys.file_exists moopath) then
raise (IncludedFileNotCompiled moopath);
(match types with (name,_,_,_)::_ -> name | _ -> assert false)
| _ -> assert false in
let uri =
- UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext)
+ UriManager.uri_of_string (MatitaTypes.qualify status name ^ ext)
in
- let metasenv = MatitaMisc.get_proof_metasenv status in
+ let metasenv = MatitaTypes.get_proof_metasenv status in
match obj with
| Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
let name = UriManager.name_of_uri uri in
proof_status = No_proof;
options = default_options ();
objects = [];
+ coercions = [];
notation_ids = [];
}