diff options
| author | msozeau | 2008-03-07 16:32:12 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-07 16:32:12 +0000 |
| commit | ec850ff623801e514b3ed0a42beb6f7984992520 (patch) | |
| tree | 6a03dd3d0545b927326f28e7d8da08a850cead5f /contrib/interface | |
| parent | 905c47d6a07cc69b9e7aa0b9d73caeacf2b1d2be (diff) | |
Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part
of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/depends.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 7 |
2 files changed, 5 insertions, 4 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index 77d405e15d..a0cbe22b36 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -363,7 +363,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacTransitivity c -> depends_of_'constr c acc (* Equality and inversion *) - | TacRewrite (_,cbl,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc + | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc | TacInversion (is, _) -> depends_of_'a_'b_inversion_strength depends_of_'constr is acc (* For ML extensions *) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 4d28a22a98..c5a8c756a8 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1011,14 +1011,15 @@ and xlate_tac = CT_coerce_TACTIC_COM_to_TACTIC_OPT tac in CT_replace_with (c1, c2,cl,tac_opt) - | TacRewrite(false,[b,Precisely 1,cbindl],cl) -> + | TacRewrite(false,[b,Precisely 1,cbindl],cl,None) -> let cl = xlate_clause cl and c = xlate_formula (fst cbindl) and bindl = xlate_bindings (snd cbindl) in if b then CT_rewrite_lr (c, bindl, cl) else CT_rewrite_rl (c, bindl, cl) - | TacRewrite(false,_,cl) -> xlate_error "TODO: rewrite of several hyps at once" - | TacRewrite(true,_,cl) -> xlate_error "TODO: erewrite" + | TacRewrite(_,_,_,Some _) -> xlate_error "TODO: rewrite by" + | TacRewrite(false,_,cl,_) -> xlate_error "TODO: rewrite of several hyps at once" + | TacRewrite(true,_,cl,_) -> xlate_error "TODO: erewrite" | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) -> let t = out_gen rawwit_main_tactic t in let b = out_gen Extraargs.rawwit_orient b in |