G.NObj (loc,
N.Theorem(name, N.Implicit `JustOne, Some body, attrs),
true)
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 ->
let attrs = src, `Axiom, `Regular in
G.NObj (loc, N.Theorem (name, typ, None, attrs),i)
| src = source; IDENT "inductive"; spec = inductive_spec ->
paramspec = OPT inverter_param_list ;
outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
G.NInverter (loc,name,indty,paramspec,outsort)
paramspec = OPT inverter_param_list ;
outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
G.NInverter (loc,name,indty,paramspec,outsort)
let urify = function
| NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
let urify = function
| NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
| IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
G.UnificationHint (loc, t, n)
| IDENT "coercion"; name = IDENT;
| IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
G.UnificationHint (loc, t, n)
| IDENT "coercion"; name = IDENT;