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"; xt = OPT [ t = tactic_term -> t ] ->
- GrafiteAst.Destruct (loc, xt)
+ | 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 ->
let arity = match arity with None -> 0 | Some x -> x in
let saturations = match saturations with None -> 0 | Some x -> x in
let arity = match arity with None -> 0 | Some x -> x in
let saturations = match saturations with None -> 0 | Some x -> x in
- (loc, UriManager.uri_of_string suri, true, arity, saturations)
+ (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 "." ->