* http://helm.cs.unibo.it/
*)
-(* $Id$ *)
+(* $Id: grafiteParser.ml 13176 2016-04-18 15:29:33Z fguidi $ *)
module N = NotationPt
module G = GrafiteAst
| SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
| SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
| SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
+ | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that"; IDENT
+ "is"; IDENT "equivalent"; "to"; t' = tactic_term -> t'] -> G.NTactic (loc,[G.Suppose (loc,t,id,t1)])
]
];
auto_fixed_param: [
G.NObj (loc,
N.Theorem(name, N.Implicit `JustOne, Some body, attrs),
true)
- | src = source; IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
+ | src = source; IDENT "axiom"; i = index; name = IDENT;
+ params = LIST0 protected_binder_vars; SYMBOL ":"; typ = term -> (* FG: params added *)
+ let typ = shift_params `Forall params typ in
let attrs = src, `Axiom, `Regular in
G.NObj (loc, N.Theorem (name, typ, None, attrs),i)
| src = source; IDENT "inductive"; spec = inductive_spec ->