--- /dev/null
+matita : current version: 0.99.3
+matitaB: new version: 0.5.8
+helm : old version: 0.5.8 with additional material
?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts
=
content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
+(* FG: prec not optional in my patch *)
(fun ?(prec=90) annterm ->
let ast, ids_to_uris =
TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
* http://helm.cs.unibo.it/
*)
-(* $Id$ *)
+(* $Id: grafiteParser.ml 13176 2016-04-18 15:29:33Z fguidi $ *)
module N = NotationPt
module G = GrafiteAst
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 ->