diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 1974d8bc..cba2e7d0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_tactic.ml4 8651 2006-03-21 21:54:43Z jforest $ *) +(* $Id: g_tactic.ml4 8878 2006-05-30 16:44:25Z herbelin $ *) open Pp open Pcoq @@ -102,7 +102,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) = (id,n,CProdN(loc,bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = - let _ = option_app (fun (aloc,_) -> + let _ = option_map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofix_tac", Pp.str"Annotation forbidden in cofix expression")) ann in @@ -121,8 +121,8 @@ GEXTEND Gram simple_intropattern; int_or_var: - [ [ n = integer -> Genarg.ArgArg n - | id = identref -> Genarg.ArgVar id ] ] + [ [ n = integer -> Rawterm.ArgArg n + | id = identref -> Rawterm.ArgVar id ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: @@ -155,11 +155,11 @@ GEXTEND Gram conversion: [ [ c = constr -> (None, c) | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2) - | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr -> + | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr -> (Some (nl,c1), c2) ] ] ; occurrences: - [ [ "at"; nl = LIST1 integer -> nl + [ [ "at"; nl = LIST1 int_or_var -> nl | -> [] ] ] ; pattern_occ: @@ -240,7 +240,7 @@ GEXTEND Gram ] ] ; hypident_occ: - [ [ (id,l)=hypident; occs=occurrences -> (id,occs,l) ] ] + [ [ (id,l)=hypident; occs=occurrences -> ((occs,id),l) ] ] ; clause: [ [ "in"; "*"; occs=occurrences -> @@ -261,6 +261,11 @@ GEXTEND Gram [ [ "in"; idl = LIST1 id_or_meta -> idl | -> [] ] ] ; + orient: + [ [ "->" -> true + | "<-" -> false + | -> true ]] + ; fixdecl: [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot; ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] @@ -285,7 +290,8 @@ GEXTEND Gram [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ] ; by_tactic: - [ [ IDENT "by"; tac = tactic -> TacComplete tac | -> TacId [] ] ] + [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac + | -> TacId [] ] ] ; simple_tactic: [ [ @@ -411,6 +417,8 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) + | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> + TacRewrite (b,c,cl) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion |