content2Procedural.ml: "Intros+LetTac" ok

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 

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index efc0078862b6ad3bdc43a9a33699d6e3873d8a18..0704863f5a779ee28282863c16b38741221ee6a6 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -33,7 +33,7 @@ let tactical_terminator = ""
 let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
 
-let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
+let pp_idents idents = "(" ^ String.concat " " idents ^ ")"
 
 let pp_reduction_kind ~term_pp = function
   | `Normalize -> "normalize"
@@ -298,9 +298,9 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
-  | Note (_,str) -> sprintf "(* %s *)" str
+  | Note (_,str) -> sprintf "(* %s *)\n" str
   | Code (_,code) ->
-      sprintf "(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
+      sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
 
 let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
   function

diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index 67c4b1ebf8a9d41b96f28fe63d932dd8d401955d..93b1959905a2740f5552faa94441f123616fcc68 100644 (file)
--- a/helm/software/matita/contribs/prova.ma
+++ b/helm/software/matita/contribs/prova.ma
@@ -14,5 +14,12 @@
 
 set "baseuri" "cic:/matita/tests".
 
+alias id "subst0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1)".
+alias id "pr0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1)".
+alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
+alias id "T" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1)".
+
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".