diff options
| author | letouzey | 2008-03-01 01:59:59 +0000 |
|---|---|---|
| committer | letouzey | 2008-03-01 01:59:59 +0000 |
| commit | 0d62e3344d7f69c0296c347c7aeddabd09bbab60 (patch) | |
| tree | 38032050565becc6868e462956caeca0367c3a0a /parsing/pptactic.ml | |
| parent | 50d4df2da89461f280c302d032422856f8e77991 (diff) | |
Rework on rich forms of rewrite
1) changed the semantics of rewrite H,H' : the earlier semantics
(rewrite H,H' == rewrite H; rewrite H') was poorly suited for
situations where first rewrite H generates side-conditions.
New semantics is tclTHENFIRST instead of tclTHEN, that is
side-conditions are left untouched.
Note to myself: check if side-effect-come-first bug of
setoid rewrite is still alive, and do something if yes
2) new syntax for rewriting something many times. This syntax is
shamelessly taken from ssreflect:
rewrite ?H means "H as many times as possible"
(i.e. almost repeat rewrite H, except that
possible side-conditions are left apart as in 1)
rewrite !H means "at least once" (i.e. rewrite H; repeat rewrite H)
rewrite 3?H means "up to 3 times", maybe less
(i.e. something like: do 3 (try rewrite H)).
rewrite 3!H means "exactly 3 times" (i.e. almost do 3 rewrite H).
For instance: rewrite 3?foo, <-2!bar in H1,H2|-*
3) By the way, for a try, I've enabled the syntax +/- as synonyms for
->/<- in the orientation of rewrite.
Comments welcome ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10612 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 10 |
1 files changed, 9 insertions, 1 deletions
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) -> |