*)
open Printf
+
open MatitaTypes
exception Drop;;
let set_goals (status,_) goals = status,goals
let id_tac status =
- apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status
+ apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) status
let mk_tactic tac = tac
List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
status new_coercions in
let statement_of name =
- GrafiteAstPp.pp_statement
- (GrafiteAst.Executable (Disambiguate.dummy_floc,
- (GrafiteAst.Command (Disambiguate.dummy_floc,
- (GrafiteAst.Coercion (Disambiguate.dummy_floc,
- (CicNotationPt.Ident (name, None)))))))) ^ "\n"
+ GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
+ (CicNotationPt.Ident (name, None)))
in
- let moo_content_rev =
- [statement_of (UriManager.name_of_uri coer_uri)] @
+ let moo_content =
+ statement_of (UriManager.name_of_uri coer_uri) ::
(List.map
(fun (uri, _, _) ->
statement_of (UriManager.name_of_uri uri))
- new_coercions) @ status.moo_content_rev
+ new_coercions)
in
- let status = {status with moo_content_rev = moo_content_rev} in
- {status with proof_status = No_proof}
+ let status = add_moo_content moo_content status in
+ { status with proof_status = No_proof }
let generate_elimination_principles uri status =
let elim sort status =
match cmd with
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
- {status with moo_content_rev =
- (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
+ 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
| GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
| GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *)
| GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
- let status' =
- { status with
- moo_content_rev =
- (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
- in
+ let status' = add_moo_content [stm] status in
let aliases' =
DisambiguateTypes.Environment.cons
(DisambiguateTypes.Symbol (symbol, 0))
status.aliases
in
MatitaSync.set_proof_aliases status' aliases'
- | GrafiteAst.Notation _ as stm ->
- { status with moo_content_rev =
- (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
+ | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
| GrafiteAst.Obj (loc,obj) ->
let ext,name =
match obj with