+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ->
+ G.NTactic (loc,[G.We_need_to_prove (loc, t, id)])
+ | IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t = tactic_term -> G.NTactic(loc,[G.BetaRewritingStep (loc,t)])
+ | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t1=tactic_term -> G.NTactic (loc,[G.Thesisbecomes(loc,t1)])
+ | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ G.NTactic (loc,[G.We_proceed_by_cases_on (loc, t, t1)])
+ | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ G.NTactic (loc,[G.We_proceed_by_induction_on (loc, t, t1)])
+ | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ G.NTactic (loc,[G.Byinduction(loc, t, id)])
+ | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
+ SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
+ G.NTactic (loc,[G.Case(loc,id,params)])
+ | IDENT "print_stack" -> G.NTactic (loc,[G.PrintStack loc])
+ (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
+(*
+ | IDENT "conclude";
+ termine = tactic_term;
+ SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | 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;
+ termine = tactic_term;
+ SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | 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)])
+*)
+ | IDENT "obtain" ; name = IDENT;
+ termine = tactic_term ->
+ G.NTactic(loc,[G.Obtain(loc, name, termine)])
+ | IDENT "conclude" ; termine = tactic_term ->
+ G.NTactic(loc,[G.Conclude(loc, termine)])
+ | SYMBOL "=" ;
+ t1=tactic_term ;
+ t2 =
+ [ IDENT "using"; t=tactic_term -> `Term t
+ | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | 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, t1, t2, cont)])