diff options
| author | barras | 2002-03-05 10:59:15 +0000 |
|---|---|---|
| committer | barras | 2002-03-05 10:59:15 +0000 |
| commit | 70894b275f1dbaf73d54770bb4311a146c9514d8 (patch) | |
| tree | 03156f2c948758a8bfc54c9855d5f4d32b16896e | |
| parent | 4dbf6842e0b2b43c5f8c15817942dfecaab5cd2e (diff) | |
assert failure avec Conditional Rewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2513 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/equality.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index ee01a3b1fd..de98abd610 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -106,8 +106,8 @@ let dyn_conditional_rewrite lft2rgt = function tactic_com_bind_list (conditional_rewrite lft2rgt (Tacinterp.interp tac)) (com,binds) - | [(Tacexp tac); (Constr c);(Cbindings binds)] -> - conditional_rewrite lft2rgt (Tacinterp.interp tac) (c,binds) + | [(Tac (tac,_)); (Constr c);(Cbindings binds)] -> + conditional_rewrite lft2rgt tac (c,binds) | _ -> assert false let v_rewriteLR = hide_tactic "RewriteLR" dyn_rewriteLR @@ -162,8 +162,8 @@ let dyn_conditional_rewrite_in lft2rgt = function tactic_com_bind_list (conditional_rewrite_in lft2rgt id (Tacinterp.interp tac)) (com,binds) - | [(Tacexp tac); Identifier id; (Constr c);(Cbindings binds)] -> - conditional_rewrite_in lft2rgt id (Tacinterp.interp tac) (c,binds) + | [(Tac (tac,_)); Identifier id; (Constr c);(Cbindings binds)] -> + conditional_rewrite_in lft2rgt id tac (c,binds) | _ -> assert false let rewriteLR_in_tac = hide_tactic "RewriteLRin" (dyn_rewrite_in true) |