X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=1b60e99026b9fef75f4f8ab2d85db8ecfb8fe34b;hb=3fab56d1663ba3d5aeb9207612279e0bb0edbb8c;hp=714cb48263c2616831b1cf2933c65ec93fabebc3;hpb=dd627e471392375ca7b6dad78a931a8682e06dbe;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 714cb4826..1b60e9902 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -272,6 +272,7 @@ EXTEND
     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term ; t2 = OPT [IDENT "or"; IDENT
     "equivalently"; t2 = tactic_term -> t2] ->
         G.NTactic (loc,[G.Thesisbecomes(loc,t1,t2)])
+    | IDENT "print_stack" -> G.NTactic (loc,[G.PrintStack loc])
     (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
     | IDENT "conclude";  
       termine = tactic_term;
@@ -281,7 +282,16 @@ EXTEND
        [ IDENT "using"; t=tactic_term -> `Term t
        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
        | IDENT "proof" -> `Proof
-       | params = auto_params -> let _,params = params in `Auto params];
+       | params = auto_params -> `Auto 
+            (
+               let just,params = params in
+               match just with 
+                 | None -> (None,params)
+                 | Some (`Univ univ) -> (Some univ,params)
+                 (* `Trace behaves exaclty like None for the moment being *)
+                 | Some (`Trace) -> (None,params)
+             )
+       ];
       cont = rewriting_step_continuation ->
        G.NTactic (loc,[G.RewritingStep(loc, Some (None,termine), t1, t2, cont)])
     | IDENT "obtain" ; name = IDENT;
@@ -292,7 +302,16 @@ EXTEND
        [ IDENT "using"; t=tactic_term -> `Term t
        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
        | IDENT "proof" -> `Proof
-       | params = auto_params -> let _,params = params in `Auto params];
+       | params = auto_params -> `Auto 
+            (
+               let just,params = params in
+               match just with 
+                 | None -> (None,params)
+                 | Some (`Univ univ) -> (Some univ,params)
+                 (* `Trace behaves exaclty like None for the moment being *)
+                 | Some (`Trace) -> (None,params)
+             )
+       ];
       cont = rewriting_step_continuation ->
        G.NTactic(loc,[G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)])
     | SYMBOL "=" ;
@@ -301,7 +320,16 @@ EXTEND
        [ IDENT "using"; t=tactic_term -> `Term t
        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
        | IDENT "proof" -> `Proof
-       | params = auto_params -> let _,params = params in `Auto params];
+       | params = auto_params -> `Auto 
+            (
+               let just,params = params in
+               match just with 
+                 | None -> (None,params)
+                 | Some (`Univ univ) -> (Some univ,params)
+                 (* `Trace behaves exaclty like None for the moment being *)
+                 | Some (`Trace) -> (None,params)
+             )
+       ];
       cont = rewriting_step_continuation ->
        G.NTactic(loc,[G.RewritingStep(loc, None, t1, t2, cont)])
     ]