Huge commit:

[helm.git] / components / content_pres / content2Procedural.ml

diff --git a/components/content_pres/content2Procedural.ml b/components/content_pres/content2Procedural.ml
index 8306ea286ed59d8442885814f924dd2a8cdc99b2..66a4370f36eca1e79ff702e17a3bb59b3b456e32 100644 (file)
--- 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