fixed Whelp stuff

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9b0617bc8010482decadcd1c31363ea5f7c9d3b8..5e70ff571ecd62b8a3402da395c8aebee9b5312a 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -485,9 +485,15 @@ EXTEND
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
-        TacticAst.Match (loc,t)
+        TacticAst.WMatch (loc,t)
     | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
-        TacticAst.Instance (loc,t)
+        TacticAst.WInstance (loc,t)
+    | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> 
+        TacticAst.WLocate (loc,id)
+    | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
+        TacticAst.WElim (loc, t)
+    | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
+        TacticAst.WHint (loc,t)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
   ]];
 

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index ef79ab4ad254aebac239a96dbf31f83281565e59..fdffe82760b840622a2f33829903e7d13abee456 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -261,7 +261,7 @@ and proof2pres term2pres p =
              [B.H([Some "helm", "xref", "ce_"^hd_xref],
                [ce2pres hd]);
              continuation'])
-         
+        
   and ce2pres =
     let module Con = Content in
       function
@@ -304,8 +304,10 @@ and proof2pres term2pres p =
                    term])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | `Joint ho -> 
-            B.Text ([],"jointdef")
+      | `Joint ho -> assert false (*
+        B.H ([],
+        (B.Text ([],"JOINT ")
+        :: List.map ce2pres ho.Content.joint_defs)) *)
 
   and acontext2pres ac continuation indent =
     let module Con = Content in
@@ -380,7 +382,11 @@ and proof2pres term2pres p =
       let arg = 
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
-         | _ -> assert false) in
+         | [Con.Premise p] -> 
+             (match p.Con.premise_binder with
+             | None -> assert false; (* unnamed hypothesis ??? *)
+             | Some s -> B.Text([],s))
+         | err -> assert false) in
       (match conclude.Con.conclude_conclusion with 
          None ->
           B.b_h [] [B.b_kw "Consider"; B.b_space; arg]

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 692d4679e85b012e6da2018d38815c7983b9fae0..ae9143dabf849ed29f1d9c5c9e41b2f8114c9230 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -92,12 +92,17 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 type print_kind = [ `Env | `Coer ]
 
 type 'term macro = 
+  (* Whelp's stuff *)
+  | WHint of loc * 'term 
+  | WMatch of loc * 'term 
+  | WInstance of loc * 'term 
+  | WLocate of loc * string
+  | WElim of loc * 'term
+  (* real macros *)
   | Abort of loc
   | Print of loc * string
   | Check of loc * 'term 
   | Hint of loc
-  | Match of loc * 'term 
-  | Instance of loc * 'term 
   | Quit of loc
   | Redo of loc * int option
   | Undo of loc * int option

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 9fb8455f9260a7aaa3d1d27049a8e5ab99d712ca..f10443c2d01896c004e750b1e3903dba096c27c5 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -112,6 +112,13 @@ let pp_search_kind = function
   | `Elim -> "elim"
 
 let pp_macro pp_term = function 
+  (* Whelp *)
+  | WInstance (_, term) -> "whelp instance " ^ pp_term term
+  | WHint (_, t) -> "whelp hint " ^ pp_term t
+  | WLocate (_, s) -> "whelp locate " ^ s
+  | WElim (_, t) -> "whelp elim " ^ pp_term t
+  | WMatch (_, term) -> "whelp match " ^ pp_term term
+  (* real macros *)
   | Abort _ -> "Abort"
   | Check (_, term) -> sprintf "Check %s" (pp_term term)
   | Hint _ -> "hint"
@@ -125,8 +132,6 @@ let pp_macro pp_term = function
   | Undo (_, Some n) -> sprintf "Undo %d" n
   | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
-  | Instance _
-  | Match _ -> assert false
 
 let pp_macro_ast = pp_macro pp_term_ast
 let pp_macro_cic = pp_macro pp_term_cic