| 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;
[ 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;
[ 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 "=" ;
[ 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)])
]