Procedural: we added the support for theorem flavours and we fixed the handling ...

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index a6e0667b05de904d64209c177889ea06b3f37daa..455f714af653acf161d54aab2d67c0c24e9b5d41 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -393,8 +393,9 @@ and proc_appl st what hd tl =
    mk_preamble st what script
 
 and proc_other st what =
+   let _, dtext = test_depth st in
    let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
-   let script = [T.Note text] in
+   let script = [T.Apply (what, dtext ^ text)] in 
    mk_preamble st what script
 
 and proc_proof st t = 
@@ -456,7 +457,7 @@ let proc_obj st = function
       let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
       let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
       if st.skip_thm_and_qed then ast
-      else T.Theorem (Some s, t, "") :: ast @ [T.Qed text]
+      else T.Theorem (`Theorem, Some s, t, "") :: ast @ [T.Qed text]
    | _                                                               ->
       failwith "not a theorem"
 

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 6534b872538b0912e4e1d8ce75fa72a2a434a604..b0820f225af0ad2da3468359d29c03816a2136e2 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -54,6 +54,7 @@ let list_init f i =
 
 (****************************************************************************)
 
+type flavour  = Cic.object_flavour
 type name     = string option
 type hyp      = string
 type what     = Cic.annterm
@@ -66,7 +67,7 @@ type inferred = Cic.annterm
 type pattern  = Cic.annterm
 
 type step = Note of note 
-          | Theorem of name * what * note
+          | Theorem of flavour * name * what * note
           | Qed of note
          | Id of note
          | Intros of count option * name list * note
@@ -99,9 +100,9 @@ let mk_notenote str a =
 let mk_thnote str a =
    if str = "" then a else mk_note "" :: mk_note str :: a
 
-let mk_theorem name t =
+let mk_theorem flavour name t =
    let name = match name with Some name -> name | None -> assert false in
-   let obj = N.Theorem (`Theorem, name, t, None) in
+   let obj = N.Theorem (flavour, name, t, None) in
    G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
 
 let mk_qed =
@@ -182,7 +183,7 @@ let mk_vb = G.Shift floc
 
 let rec render_step sep a = function
    | Note s                  -> mk_notenote s a
-   | Theorem (n, t, s)       -> mk_theorem n t :: mk_thnote s a 
+   | Theorem (f, n, t, s)    -> mk_theorem f n t :: mk_thnote s a 
    | Qed s                   -> mk_qed :: mk_tacnote s a
    | Id s                    -> mk_id sep :: mk_tacnote s a
    | Intros (c, ns, s)       -> mk_intros c ns sep :: mk_tacnote s a

diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli
index c493873ff2b0fd736c56d5fc26082f9acb811b48..68c4ce709ad333087aaab8d8c361f7a1ae551285 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.mli
+++ b/helm/software/components/acic_procedural/proceduralTypes.mli
@@ -33,6 +33,7 @@ val mk_arel: int -> string -> Cic.annterm
 
 (****************************************************************************)
 
+type flavour  = Cic.object_flavour
 type name     = string option
 type hyp      = string
 type what     = Cic.annterm
@@ -45,7 +46,7 @@ type inferred = Cic.annterm
 type pattern  = Cic.annterm
 
 type step = Note of note 
-          | Theorem of name * what * note
+          | Theorem of flavour * name * what * note
           | Qed of note
          | Id of note
          | Intros of count option * name list * note