| _ ->
(*CSC: new NCicPp.status is the best I can do here without changing the
result type *)
- raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term (new NCicPp.status) params)) ]
+ raise (Invalid_argument ("malformed target parameter list 2\n" ^
+ NotationPp.pp_term (new NCicPp.status None ) params)) ]
];
direction: [
[ SYMBOL ">" -> `LeftToRight
| None ->
G.NTactic(loc,
[G.NAuto(loc,(None,["depth",depth]@params))])
- | Some (`Univ univ) ->
+ | Some (b,`Univ univ) ->
G.NTactic(loc,
- [G.NAuto(loc,(Some univ,["depth",depth]@params))])
- | Some `EmptyUniv ->
+ [G.NAuto(loc,(Some (b,univ),["depth",depth]@params))])
+ | Some (b,`EmptyUniv) ->
G.NTactic(loc,
- [G.NAuto(loc,(Some [],["depth",depth]@params))])
- | Some `Trace ->
+ [G.NAuto(loc,(Some (b,[]),["depth",depth]@params))])
+ | Some (b,`Trace) ->
G.NMacro(loc,
G.NAutoInteractive (loc, (None,["depth",depth]@params))))
| IDENT "intros" -> G.NMacro (loc, G.NIntroGuess loc)
- | IDENT "check"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
+ | IDENT "check"; t = tactic_term -> G.NMacro(loc,G.NCheck (loc,t))
| IDENT "screenshot"; fname = QSTRING ->
G.NMacro(loc,G.Screenshot (loc, fname))
| IDENT "cases"; what = tactic_term ; where = pattern_spec ->
i = auto_fixed_param -> i,""
| i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
string_of_int v | v = IDENT -> v ] -> i,v ];
- just = OPT [ IDENT "by"; by =
- [ univ = tactic_term_list1 -> `Univ univ
- | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
- | SYMBOL "_" -> `Trace ] -> by ] -> just,params
+ just = OPT [ is_user_trace =
+ [ IDENT "by" -> true
+ | IDENT "trace" -> false ];
+ by =
+ [ univ = tactic_term_list1 -> `Univ univ
+ | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
+ | SYMBOL "_" -> `Trace ] -> is_user_trace,by ] -> just,params
]
];
]];
grafite_ncommand: [ [
- IDENT "qed" -> G.NQed loc
+ IDENT "qed" ; b = OPT SYMBOL "-" ->
+ let b = match b with None -> true | Some _ -> false in G.NQed (loc,b)
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
G.NUnivConstraint (loc,u1,u2)
| IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
G.UnificationHint (loc, t, n)
- | IDENT "coercion"; name = IDENT; SYMBOL ":"; ty = term;
+ | IDENT "coercion"; name = IDENT; spec = OPT [ SYMBOL ":"; ty = term;
SYMBOL <:unicode<def>>; t = term; "on";
id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
- "to"; target = term ->
- G.NCoercion(loc,name,t,ty,(id,source),target)
+ "to"; target = term -> t,ty,(id,source),target ] ->
+ G.NCoercion(loc,name,spec)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
G.NObj (loc, N.Record (params,name,ty,fields))
| IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with";
method parser_db: db
end
-class virtual status =
+class virtual status uid =
object(self)
- inherit CicNotationParser.status ~keywords:[]
+ inherit CicNotationParser.status uid ~keywords:[]
val mutable db = None (* mutable only to initialize it :-( *)
method parser_db = match db with None -> assert false | Some x -> x
method set_parser_db v = {< db = Some v >}
;;
-let parse_statement status =
+let parse_statement status =
+ status#reset_loctable ();
parse_statement status#parser_db
(* vim:set foldmethod=marker: *)