content2Procedural.ml: "Intros+LetTac" ok

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

diff --git a/helm/software/components/content_pres/content2Procedural.ml b/helm/software/components/content_pres/content2Procedural.ml
index 66a4370f36eca1e79ff702e17a3bb59b3b456e32..99fe8d0b250b9e647fe46f260b6b5b023e63eeb6 100644 (file)
--- a/helm/software/components/content_pres/content2Procedural.ml
+++ b/helm/software/components/content_pres/content2Procedural.ml
@@ -39,22 +39,43 @@ let mk_theorem name t =
    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 sep = G.Dot floc in
+   G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), Some sep))
 
+let mk_intros xi ids =
+   let tactic = G.Intros (floc, xi, ids) in
+   mk_tactic tactic
+   
 let mk_exact t =
    let tactic = G.Exact (floc, t) in
    mk_tactic tactic
 
+(* internal functions *******************************************************)
+
+let mk_intros_arg = function
+   | `Declaration {C.dec_name = Some name}
+   | `Hypothesis {C.dec_name = Some name}
+   | `Definition {C.def_name = Some name} -> name 
+   | _ -> assert false
+
+let mk_intros_args pc = List.map mk_intros_arg pc
+
+let rec mk_proof p = 
+   let cmethod = p.C.proof_conclude.C.conclude_method in
+   let cargs = p.C.proof_conclude.C.conclude_args in
+   match cmethod, cargs with
+      | "Intros+LetTac", [C.ArgProof q] -> 
+         let names = mk_intros_args q.C.proof_context in
+        let num = List.length names in
+        let text = String.concat " " names in
+        mk_intros (Some num) [] :: mk_note text :: mk_proof q
+      | _ -> [mk_note (Printf.sprintf "%s %u" cmethod (List.length cargs))] 
+
 (* interface functions ******************************************************)
 
 let content2procedural ~ids_to_inner_sorts prefix (_, params, xmenv, obj) = 
    if List.length params > 0 || xmenv <> None then assert false;
    match obj with
-      | `Def (C.Const, t, `Proof {
-           C.proof_name = Some name; C.proof_context = []; 
-          C.proof_apply_context = []; C.proof_conclude = {
-             C.conclude_conclusion = Some b
-          }
-        }) ->  
-       [mk_theorem name t; mk_exact b]
+      | `Def (C.Const, t, `Proof ({C.proof_name = Some name} as p)) ->
+           mk_theorem name t :: mk_proof p
       | _ -> assert false