let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
-let default_precedence = 50
let default_associativity = Gramext.NonA
let mk_rec_corec ind_kind defs loc =
EXTEND
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
- tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
+ tactic_term: [ [ t = term LEVEL "90" -> t ] ];
new_name: [
[ id = IDENT -> Some id
| SYMBOL "_" -> None ]
];
notation: [
[ dir = OPT direction; s = QSTRING;
- assoc = OPT associativity; prec = OPT precedence;
+ assoc = OPT associativity; prec = precedence;
IDENT "for";
p2 =
[ blob = UNPARSED_AST ->
| None -> default_associativity
| Some assoc -> assoc
in
- let prec =
- match prec with
- | None -> default_precedence
- | Some prec -> prec
- in
let p1 =
add_raw_attribute ~text:s
- (CicNotationParser.parse_level1_pattern
+ (CicNotationParser.parse_level1_pattern prec
(Ulexing.from_utf8_string s))
in
(dir, p1, assoc, prec, p2)
| com = comment ->
fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
+ !out fname;
fun ?(never_include=false) ~include_paths status ->
let _root, buri, fullpath, _rrelpath =
Librarian.baseuri_of_script ~include_paths fname
else LexiconEngine.eval_command status
(LexiconAst.Include (iloc,buri,mode,fullpath))
in
- !out fname;
status,
LSome
(GrafiteAst.Executable