X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=components%2Fcontent_pres%2Fcontent2Procedural.ml;h=66a4370f36eca1e79ff702e17a3bb59b3b456e32;hb=6bb370c6e1a036e82315765d6dceb1939c30ed23;hp=8306ea286ed59d8442885814f924dd2a8cdc99b2;hpb=e9b482856904b32a5c92eee8bcd860ffe74fa74f;p=helm.git

diff --git a/components/content_pres/content2Procedural.ml b/components/content_pres/content2Procedural.ml
index 8306ea286..66a4370f3 100644
--- a/components/content_pres/content2Procedural.ml
+++ b/components/content_pres/content2Procedural.ml
@@ -26,28 +26,26 @@
 module H = HExtlib
 module C = Content
 module G = GrafiteAst
+module N = CicNotationPt
 
 (* grafite ast constructors *************************************************)
 
 let floc = H.dummy_floc
 
 let mk_note str = G.Comment (floc, G.Note (floc, str))
-   
-(* interface functions ******************************************************)
 
-let out_arg = function
-   | C.Aux _       -> "aux"
-   | C.Premise _   -> "premise"
-   | C.Lemma _     -> "lemma"
-   | C.Term _      -> "term"
-   | C.ArgProof _  -> "proof"
-   | C.ArgMethod _ -> "method"
+let mk_theorem name t = 
+   let obj = N.Theorem (`Theorem, name, t, None) in
+   G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
+
+let mk_tactic tactic =
+   G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None))
 
-let out_args args = String.concat " " (List.map out_arg args) 
+let mk_exact t =
+   let tactic = G.Exact (floc, t) in
+   mk_tactic tactic
 
-let out_name = function
-   | None     -> ""
-   | Some str -> str
+(* interface functions ******************************************************)
 
 let content2procedural ~ids_to_inner_sorts prefix (_, params, xmenv, obj) = 
    if List.length params > 0 || xmenv <> None then assert false;
@@ -58,5 +56,5 @@ let content2procedural ~ids_to_inner_sorts prefix (_, params, xmenv, obj) =
 	      C.conclude_conclusion = Some b
 	   }
         }) -> 	
-	[mk_note (Printf.sprintf "%s" name)]
+	[mk_theorem name t; mk_exact b]
       | _ -> assert false