Axioms are not allowed with the syntax: "axiom name: type.".

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 590de7c5462f4fe5b097113f19ff20133da23a5d..fb38674dfb2cce12e406af6ab3b985b4964ffa8e 100644 (file)
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -258,6 +258,7 @@ let pp_flavour = function
   | `Remark -> "remark"
   | `Theorem -> "theorem"
   | `Variant -> "variant"
+  | `Axiom -> "axiom"
 
 let pp_fields fields =
   (if fields <> [] then "\n" else "") ^ 

diff --git a/components/acic_content/cicNotationPt.ml b/components/acic_content/cicNotationPt.ml
index a66aa5febb3aa86600fdf8320edb439fb98ed2d0..609fb9d2f24a08f362c2276afa16f8fa2f673737 100644 (file)
--- a/components/acic_content/cicNotationPt.ml
+++ b/components/acic_content/cicNotationPt.ml
@@ -171,7 +171,8 @@ type obj =
        * - name is absent when an unnamed theorem is being proved, tipically in
        *   interactive usage
        * - body is present when its given along with the command, otherwise it
-       *   will be given in proof editing mode using the tactical language
+       *   will be given in proof editing mode using the tactical language,
+       *   unless the flavour is an Axiom
        *)
   | Record of (string * term) list * string * term * (string * term * bool) list
       (** left parameters, name, type, fields *)

diff --git a/components/cic/cic.ml b/components/cic/cic.ml
index 1becd44428bd3b4f9139c01280e0d47ef48de26e..20a6cb457dec63c700283ac952204357c38ab0de 100644 (file)
--- a/components/cic/cic.ml
+++ b/components/cic/cic.ml
@@ -62,6 +62,7 @@ type object_flavour =
   | `Remark
   | `Theorem
   | `Variant
+  | `Axiom
   ]
 
 type object_class =

diff --git a/components/cic/cicParser.ml b/components/cic/cicParser.ml
index f9d6d880ed122be497f803d4841ecd3fca478cb5..1e9a3a33c1444a553f9b7beaa8b5bee709a58254 100644 (file)
--- a/components/cic/cicParser.ml
+++ b/components/cic/cicParser.ml
@@ -672,6 +672,7 @@ let end_element ctxt tag =
         | [ "value", "remark"] -> Obj_flavour `Remark
         | [ "value", "theorem"] -> Obj_flavour `Theorem
         | [ "value", "variant"] -> Obj_flavour `Variant
+        | [ "value", "axiom"] -> Obj_flavour `Axiom
         | _ -> attribute_error ())
   | "class" ->
       let class_modifiers = pop_class_modifiers ctxt in

diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml
index 7e97dea6fb0b5fef93d430632c901f8e043688b7..95f92346bcdb066e24ea9f979a8274f294cc77a8 100644 (file)
--- a/components/cic_acic/cic2Xml.ml
+++ b/components/cic_acic/cic2Xml.ml
@@ -293,6 +293,7 @@ let xml_of_attrs attributes =
     | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
     | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
     | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
+    | `Axiom -> Xml.xml_empty "flavour" [None, "value", "axiom"]
   in
   let xml_attr_of = function
     | `Generated -> Xml.xml_empty "generated" []

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index d3af052564b5e206303d8adb7338203f6f280592..85f05aa1c8700048224840ed34f262f21e0e29f8 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -506,10 +506,13 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
      let attrs = [`Flavour flavour] in
      let ty' = interpretate_term [] env None false ty in
-     (match bo with
-        None ->
+     (match bo,flavour with
+        None,`Axiom ->
+         Cic.Constant (name,None,ty',[],attrs)
+      | Some bo,`Axiom -> assert false
+      | None,_ ->
          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
-      | Some bo ->
+      | Some bo,_ ->
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))
           

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index e83152226f257cb21132fbb3abee6b0f3c271ae7..1b06b81c97fd64b26b4429956c25e9c573c7bdd5 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -472,6 +472,8 @@ EXTEND
       body = term ->
         GrafiteAst.Obj (loc,
           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
+    | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
+        GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
           let name,ty = 

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 2dcd6a8b9c8b4c4aae69a4ccadd4cf81c8529b75..a09baafe1a99fe8e3fdc1aeed08451bbc706dd9d 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -84,7 +84,7 @@ let save_object_to_disk uri obj ugraph univlist =
   (univgraphuri,xmlunivgraphpath) ::
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
-       None,None -> []
+       None,_ -> []
      | Some bodyxml,Some bodyuri->
          ensure_path_exists xmlbodypath;
          Xml.pp ~gzip:true bodyxml (Some xmlbodypath);

diff --git a/matita/matita.lang b/matita/matita.lang
index 52459589eca2d7f6903dba12380dcf0abc161139..1e2f0e57c70711b1dd61d6c38852b0610b1b03a5 100644 (file)
--- a/matita/matita.lang
+++ b/matita/matita.lang
@@ -21,6 +21,7 @@
     <keyword>fact</keyword>
     <keyword>remark</keyword>
     <keyword>variant</keyword>
+    <keyword>axiom</keyword>
   </keyword-list>
     
   <keyword-list _name = "Commands" style = "Keyword" case-sensitive="TRUE">