diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 28 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 10 |
2 files changed, 32 insertions, 6 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index f305ebd69e..724bb2da1b 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -288,8 +288,10 @@ GEXTEND Gram orient: [ [ "->" -> true | "<-" -> false + | "+" -> true + | "-" -> false | -> true ]] - ; + ; fixdecl: [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot; ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] @@ -319,9 +321,25 @@ GEXTEND Gram ; rename : [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] - ; + ; rewriter : - [ [ b = orient; c = constr_with_bindings -> (b,c) ] ] + [ [ c = constr_with_bindings -> (Precisely 1, c) + | "!"; c = constr_with_bindings -> (RepeatPlus,c) + | "?"; c = constr_with_bindings -> (RepeatStar,c) + | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c) + | n = natural; "?"; c = constr_with_bindings -> (UpTo n,c) + (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally + produce a pattern_ident *) + | c = pattern_ident -> + let c = (CRef (Libnames.Ident (dummy_loc,c)), NoBindings) in + (RepeatStar, c) + | n = natural; c = pattern_ident -> + let c = (CRef (Libnames.Ident (dummy_loc,c)), NoBindings) in + (UpTo n, c) + ] ] + ; + oriented_rewriter : + [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] ; simple_tactic: [ [ @@ -451,9 +469,9 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) - | IDENT "rewrite"; l = LIST1 rewriter SEP ","; cl = clause -> + | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause -> TacRewrite (false,l,cl) - | IDENT "erewrite"; l = LIST1 rewriter SEP ","; cl = clause -> + | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause -> TacRewrite (true,l,cl) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 67858b3c60..da915a5cc3 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -428,6 +428,13 @@ let pr_clause_pattern pr_id = function let pr_orient b = if b then mt () else str " <-" +let pr_multi = function + | Precisely 1 -> mt () + | Precisely n -> pr_int n ++ str "!" + | UpTo n -> pr_int n ++ str "?" + | RepeatStar -> str "?" + | RepeatPlus -> str "!" + let pr_induction_arg prlc prc = function | ElimOnConstr c -> pr_with_bindings prlc prc c | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) @@ -818,7 +825,8 @@ and pr_atom1 = function hov 1 (str (if ev then "erewrite" else "rewrite") ++ prlist_with_sep (fun () -> str ","++spc()) - (fun (b,c) -> pr_orient b ++ spc() ++ pr_with_bindings c) + (fun (b,m,c) -> + pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c) l ++ pr_clauses pr_ident cl) | TacInversion (DepInversion (k,c,ids),hyp) -> |