X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=3eb64d458fe2892a44f32af5bb1ce5e0af0db1fb;hb=acc9067d3263ffced81c52539f918d47d418d5c7;hp=64c10b9b47e575db35b37981aa79ffc15c95d3b8;hpb=64d7a7dfa840d7279f9af64240ee1f8a69181801;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 64c10b9b4..3eb64d458 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -157,18 +157,20 @@ EXTEND
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
-        idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
-        let types = match types with None -> [] | Some types -> types in
+    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
 	let idents = match idents with None -> [] | Some idents -> idents in
-	let to_spec id = GrafiteAst.Ident id in
-	GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+	GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
-    | IDENT "elim"; what = tactic_term; using = using;
-      (num, idents) = intros_spec ->
-	GrafiteAst.Elim (loc, what, using, num, idents)
+    | IDENT "elim"; what = tactic_term; using = using; 
+       pattern = OPT pattern_spec;
+       (num, idents) = intros_spec ->
+	let pattern = match pattern with
+	   | None         -> None, [], Some Ast.UserInput
+	   | Some pattern -> pattern   
+	in
+	GrafiteAst.Elim (loc, what, using, pattern, num, idents)
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
 	GrafiteAst.ElimType (loc, what, using, num, idents)
@@ -256,12 +258,12 @@ EXTEND
 	 | BYC_weproved (ty,id,t1) ->
 	    GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
 	 | BYC_letsuchthat (id1,t1,id2,t2) ->
-	    (match t with
+	   (* (match t with
 	        LNone floc ->
                  raise (HExtlib.Localized
 		  (floc,CicNotationParser.Parse_error
 		    "tactic_term expected here"))
-              | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+              | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
 	 | BYC_wehaveand (id1,t1,id2,t2) ->
 	    (match t with
 	        LNone floc ->