*** empty log message ***

3 files changed, 56 insertions, 9 deletions

diff --git a/phox/phox-font.el b/phox/phox-font.el
index 9e330ea2..3064a855 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -12,19 +12,20 @@
     0 'font-lock-string-face t)
     (cons (concat "\\([ \t]\\|^\\)\\("
        "Cst\\|"
-       "Import\\|"
+       "Data\\|"
+       "I\\(mport\\|nductive\\)\\|"
        "Use\\|"
        "Sort\\|"
        "new_\\(intro\\|elim\\|rewrite\\)\\|"
        "a\\(dd_path\\|uthor\\)\\|"
        "c\\(laim\\|ose_def\\|or\\(ollary\\)?\\)\\|"
-       "d\\(e\\(f\\(_thlist\\)?\\|l\\)\\|ocuments\\|epend\\)\\|"
+       "d\\(e\\(f\\(_thlist\\)?\\|l\\(_proof\\)\\)\\|ocuments\\|epend\\)\\|"
        "e\\(lim_after_intro\\|xport\\|del\\|show\\)\\|"
        "f\\(act\\|lag\\)\\|"
        "goal\\|"
        "in\\(clude\\|stitute\\)\\|"
        "lem\\(ma\\)?\\|"
-       "p\\(ath\\|r\\(int\\(_sort\\)?\\|iority\\|op\\(osition\\)?\\)\\)\\|"
+       "p\\(ath\\|r\\(int\\(_sort\\)?\\|iority\\|op\\(osition\\)?\\|ove_claim\\)\\)\\|"
        "quit\\|"
        "s\\(ave\\|earch\\)\\|"
        "t\\(ex\\(_syntax\\)?\\|eheo\\(rem\\)?\\|itle\\)"
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index b349d6f3..649c18ca 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -3,6 +3,7 @@
 
 (setq
  phox-forget-id-command "del %s.\n"
+ phox-forget-proof-command "del_proof %s.\n"
  phox-forget-new-elim-command "edel elim %s.\n"
  phox-forget-new-intro-command "edel intro %s.\n"
  phox-forget-new-rewrite-command "edel rewrite %s.\n"
@@ -12,15 +13,38 @@
 ; phox-strict-comments-regexp : a not empty sequence of comments and white spaces
  phox-strict-comments-regexp "\\([ \n\t\r]+\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*\\|\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)+\\)"
  phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)"
+ phox-inductive-option "\\(\\[[^]]*]\\)?"
  phox-spaces-regexp "[ \n\t\r]*"
  phox-sy-definition-regexp (concat 
    "\\(Cst\\|def\\)"
    phox-comments-regexp
    "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") 
+ phox-sy-inductive-regexp (concat 
+   "Inductive"
+   phox-comments-regexp
+   phox-inductive-option
+   phox-comments-regexp
+   "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") 
+ phox-inductive-regexp (concat 
+   "Inductive"
+   phox-comments-regexp
+   phox-inductive-option
+   phox-comments-regexp
+   phox-ident-regexp) 
+ phox-data-regexp (concat 
+   "Data"
+   phox-comments-regexp
+   phox-inductive-option
+   phox-comments-regexp
+   phox-ident-regexp) 
  phox-definition-regexp (concat
    "\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)"
    phox-comments-regexp
    phox-ident-regexp)
+ phox-prove-claim-regexp (concat
+   "prove_claim"
+   phox-comments-regexp
+   phox-ident-regexp)
  phox-new-elim-regexp (concat
    "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
    phox-ident-regexp)
@@ -64,6 +88,7 @@
 "def"
 "def_thlist"
 "del"
+"del_proof"
 "Sort"
 "close_def"
 "edel"
@@ -84,6 +109,7 @@
 "print"
 "print_sort"
 "priority"
+"prove_claim"
 "search"
 "compile"
 "tdef"
@@ -147,8 +173,11 @@
        ((eq (span-property span 'type) 'comment))       
 
        ((eq (span-property span 'type) 'proof)
-	(setq ans (concat (format phox-forget-id-command
-				  (span-property span 'name)) ans)))
+	(if (proof-string-match phox-prove-claim-regexp str)
+	    (setq ans (concat (format phox-forget-proof-command 
+				      (match-string 4 str)) ans))
+	  (setq ans (concat (format phox-forget-id-command
+				    (span-property span 'name)) ans))))
 
        ((proof-string-match phox-new-elim-regexp str)
 	(setq ans 
@@ -175,11 +204,28 @@
 	      (concat (format phox-forget-id-command 
 				  (concat "$" (match-string 7 str))) ans)))
 
+       ((proof-string-match phox-sy-inductive-regexp str)
+	(setq ans 
+	      (concat (format phox-forget-id-command 
+				  (concat "$" (match-string 10 str))) ans)))
+
+       ((proof-string-match phox-inductive-regexp str)
+	(setq ans 
+	      (concat (format phox-forget-id-command 
+				  (match-string 8 str)) ans)))
+
+       ((proof-string-match phox-data-regexp str)
+	(setq
+	  name (match-string 8 str)
+          sname (concat (downcase (substring name 0 1)) 
+			(substring name 1 nil))
+	  ans (concat (format phox-forget-id-command 
+			      sname) ans)))
+
        ((proof-string-match phox-definition-regexp str)
 	(setq ans (concat (format phox-forget-id-command 
 				      (match-string 6 str)) ans))))
 
-
       (setq lsp (span-start span))
       (setq span (next-span span 'type)))
 
diff --git a/phox/phox.el b/phox/phox.el
index 336a1131..42ef5abd 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -107,14 +107,14 @@
    proof-comment-end               "*)"
    proof-state-command             "goals."
    proof-goal-command-regexp       
-    "\\`\\(goal\\|prop\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
+    "\\`\\(goal\\|pro\\(p\\(osition\\)?\\|ve_claim\\)\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
    proof-save-command-regexp       "\\`save"
    proof-goal-with-hole-regexp  
    (concat 
-    "\\`\\(prop\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
+    "\\`\\(pro\\(p\\(osition\\)?\\|ve_claim\\)\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
     phox-strict-comments-regexp
     phox-ident-regexp)
-   proof-goal-with-hole-result     13
+   proof-goal-with-hole-result     14
    proof-save-with-hole-regexp     
    (concat 
     "\\`save"