Some declarative tactics did not allow the "done" option in place

of "(id)". Fixed.

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 6ab2b2fc694402d63316e77b53ebf83dd2a37bce..e4b2cf24d97b3fbd3b3bb1978bdc5329f7a63600 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -88,8 +88,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   (* Costruttori Aggiunti *)
   | Assume of loc * 'ident * 'term
   | Suppose of loc * 'term *'ident * 'term option
-  | By_term_we_proved of loc *'term option * 'term * 'ident * 'term option
-  | We_need_to_prove of loc * 'term * 'ident * 'term option
+  | By_term_we_proved of loc *'term option * 'term * 'ident option * 'term option
+  | We_need_to_prove of loc * 'term * 'ident option * 'term option
   | Bydone of loc * 'term option 
   | We_proceed_by_induction_on of loc * 'term * 'term
   | Byinduction of loc * 'term * 'ident

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 547e28b3da0cac759bcd3569f13a29c22625fe1c..5644d33d3e8a0cd144a20661d18d31b026de342f 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -158,9 +158,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term 
   | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "("  ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
   | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done"
-  | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ "(" ^ident^ ")" ^
+  | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term)  ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^
        (match term2 with  None -> " " | Some term2 -> term_pp term2)
-  | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
+  | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1)
   | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1
   | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")"
   | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 5c7d31223236d3decd02fa5aa8e5a5584b8d4612..6e108ce0447109c69dab396da7faa928f1cbac89 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -55,7 +55,7 @@ let default_associativity = Gramext.NonA
 
 type by_continuation =
    BYC_done
- | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option
+ | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
  | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
  | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
 
@@ -263,7 +263,7 @@ EXTEND
                  (floc,CicNotationParser.Parse_error
                    "tactic_term expected here"))
               | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
-    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
         GrafiteAst.We_need_to_prove (loc, t, id, t1)
     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index c7e5579f8038a80a5929f261ed8d45a657c09ebd..413a43fe3a7af542838b1da2379938a85bddc90b 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -46,6 +46,7 @@ let suppose t id ty =
 ;;
 
 let by_term_we_proved ~dbd t ty id ty' =
+match id with None -> assert false | Some id ->
  let just =
   match t with
      None -> Tactics.auto ~dbd ~params:[]
@@ -75,6 +76,7 @@ let bydone ~dbd t =
 ;;
 
 let we_need_to_prove t id ty =
+match id with None -> assert false | Some id ->
  let aux status =
   let cont,cutted =
    match ty with

diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli
index e5a8a590c00b8687e62713ba9e4247e169c42f0e..3b02fb4d9c061c53a343998d433be16bab938aec 100644 (file)
--- a/components/tactics/declarative.mli
+++ b/components/tactics/declarative.mli
@@ -28,13 +28,13 @@ val assume : string -> Cic.term -> ProofEngineTypes.tactic
 val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
 
 val by_term_we_proved :
- dbd:HMysql.dbd -> Cic.term option -> Cic.term -> string -> Cic.term option ->
+ dbd:HMysql.dbd -> Cic.term option -> Cic.term -> string option -> Cic.term option ->
   ProofEngineTypes.tactic
 
 val bydone : dbd:HMysql.dbd -> Cic.term option -> ProofEngineTypes.tactic
 
 val we_need_to_prove :
- Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic
+ Cic.term -> string option -> Cic.term option -> ProofEngineTypes.tactic
 
 val we_proceed_by_induction_on : Cic.term -> Cic.term -> ProofEngineTypes.tactic