let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
- | IDENT "destruct"; t = tactic_term ->
- GrafiteAst.Destruct (loc, t)
+ | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
+ GrafiteAst.Destruct (loc, xts)
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
(num, idents) = intros_spec ->
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
(num, idents) = intros_spec ->
in
let prefix = match prefix with None -> "" | Some prefix -> prefix in
GrafiteAst.Inline (loc,style,suri,prefix)
in
let prefix = match prefix with None -> "" | Some prefix -> prefix in
GrafiteAst.Inline (loc,style,suri,prefix)
| IDENT "auto"; params = auto_params ->
GrafiteAst.AutoInteractive (loc,params)
| [ IDENT "whelp"; "match" ] ; t = term ->
| IDENT "auto"; params = auto_params ->
GrafiteAst.AutoInteractive (loc,params)
| [ IDENT "whelp"; "match" ] ; t = term ->
- GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
+ let saturations = match saturations with None -> 0 | Some x -> x in
+ let composites = match composites with None -> true | Some _ -> false in
+ GrafiteAst.Coercion
+ (loc, UriManager.uri_of_string suri, composites, arity, saturations)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
- fun ~include_paths status ->
- let buri, fullpath =
- DependenciesParser.baseuri_of_script ~include_paths fname
+ fun ?(never_include=false) ~include_paths status ->
+ let _root, buri, fullpath, _rrelpath =
+ Librarian.baseuri_of_script ~include_paths fname
- LexiconEngine.eval_command status
- (LexiconAst.Include (iloc,buri,mode,fullpath))
+ if never_include then raise (NoInclusionPerformed fullpath)
+ else LexiconEngine.eval_command status
+ (LexiconAst.Include (iloc,buri,mode,fullpath))
(loc,GrafiteAst.Command
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
(loc,GrafiteAst.Command
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->