From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 1 Aug 2018 22:30:25 +0000 (+0200)
Subject: parameter sintax added to axiom statement
X-Git-Tag: make_still_working~290
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f9abd21eb0d26cf9b632af4df819225be4d091e3

parameter sintax added to axiom statement

the syntax is already present in the other statements
---

diff --git a/README b/README
new file mode 100644
index 000000000..4aad3fc69
--- /dev/null
+++ b/README
@@ -0,0 +1,3 @@
+matita : current version: 0.99.3
+matitaB: new     version: 0.5.8
+helm   : old     version: 0.5.8  with additional material
diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index d9255f220..72f51c5f8 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -1061,6 +1061,7 @@ let content2pres
   ?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
diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index e84cd7084..be39556d8 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-(* $Id$ *)
+(* $Id: grafiteParser.ml 13176 2016-04-18 15:29:33Z fguidi $ *)
 
 module N  = NotationPt
 module G  = GrafiteAst
@@ -526,7 +526,9 @@ EXTEND
         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 ->