exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
+ (Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
disambiguate_macro:
(GrafiteTypes.status ->
(('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
disambiguate_macro:
(GrafiteTypes.status ->
(('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
options ->
GrafiteTypes.status ->
type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of (uri,arity, saturations,_) =
- GrafiteAst.Coercion
- (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
-
let basic_eval_unification_hint (t,n) status =
NCicUnifHint.add_user_provided_hint status t n
;;
let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
let status,uris =
match cmd with
- | GrafiteAst.Default (loc, what, uris) as cmd ->
- LibraryObjects.set_default what uris;
- GrafiteTypes.add_moo_content [cmd] status,`New []
| GrafiteAst.Drop loc -> raise Drop
| GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
(* Old Include command is not recursive; new one is *)