constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90" -> t ] ];
new_name: [
- [ id = IDENT -> Some id
- | SYMBOL "_" -> None ]
+ [ SYMBOL "_" -> None
+ | id = IDENT -> Some id ]
];
ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
tactic_term_list1: [
];
level3_term: [
[ u = URI -> N.UriPattern (UriManager.uri_of_string u)
+ | IMPLICIT -> N.ImplicitPattern
| id = IDENT -> N.VarPattern id
- | SYMBOL "_" -> N.ImplicitPattern
| LPAREN; terms = LIST1 SELF; RPAREN ->
(match terms with
| [] -> assert false
include_command: [ [
IDENT "include" ; path = QSTRING ->
- loc,path,L.WithPreferences
+ loc,path,false,L.WithPreferences
+ | IDENT "include" ; IDENT "source" ; path = QSTRING ->
+ loc,path,true,L.WithPreferences
| IDENT "include'" ; path = QSTRING ->
- loc,path,L.WithoutPreferences
+ loc,path,false,L.WithoutPreferences
]];
grafite_command: [ [
let stm = G.Comment (loc, com) in
!grafite_callback status stm;
status, LSome stm
- | (iloc,fname,mode) = include_command ; SYMBOL "." ->
+ | (iloc,fname,source,mode) = include_command ; SYMBOL "." ->
fun ?(never_include=false) ~include_paths status ->
let stm =
- G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
+ G.Executable (loc, G.Command (loc, G.Include (iloc, source, fname)))
in
!grafite_callback status stm;
let _root, buri, fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname
in
let stm =
- G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
+ G.Executable (loc, G.Command (loc, G.Include (iloc, source, buri)))
in
let status =
if never_include then raise (NoInclusionPerformed fullpath)