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 (file)
index 0000000..4aad3fc
--- /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 d9255f220d02247026943886f1515e96d1194a27..72f51c5f8acf261a9b453bf9f0aebeb7adf88cb3 100644 (file)
--- 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
   ?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
     (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 e84cd708495bf436cd79853ee5f8fa242b059c9d..be39556d8502fb59826083c753232a1e60148107 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
  * http://helm.cs.unibo.it/
  *)
 

-(* $Id$ *)
+(* $Id: grafiteParser.ml 13176 2016-04-18 15:29:33Z fguidi $ *)

 
 module N  = NotationPt
 module G  = GrafiteAst
 
 module N  = NotationPt
 module G  = GrafiteAst


@@ -526,7 +526,9 @@ EXTEND
         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 ->