-let concat_nuris uris nuris =
- match uris,nuris with
- | `New uris, `New nuris -> `New (nuris@uris)
- | _ -> assert false
-;;
-
-type eval_ast =
- {ea_go:
- 'term 'lazy_term 'reduction 'obj 'ident.
-
- disambiguate_command:
- (GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
-
- ?do_heavy_checks:bool ->
- GrafiteTypes.status ->
- (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
- disambiguator_input ->
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_command =
- {ec_go: 'term 'obj.
- disambiguate_command:
- (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
- options -> GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_comment =
- {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
- disambiguate_command:
- (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
- options -> GrafiteTypes.status ->
- (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-type 'a eval_executable =
- {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
-
- disambiguate_command:
- (GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
-
- options ->
- GrafiteTypes.status ->
- (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input ->
- GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
- }
-
-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)
-