diff options
| author | herbelin | 2004-03-01 17:02:00 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-01 17:02:00 +0000 |
| commit | 2a4ab4bb5720de115edb7bfbb2124194c1334cc6 (patch) | |
| tree | e4654537cc93bd87c96cb3251af6440a9d583668 /tactics/equality.ml | |
| parent | 4915bfb0184b0d5bd7016bce11743949e5dc31a3 (diff) | |
Correction sur commit précédent : Tactics.cut réduisait de manière inappropriée
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5409 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 621781187d..2f36d0c7ef 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -135,9 +135,9 @@ let abstract_replace clause c2 c1 unsafe gl = let e = (build_coq_eqT_data ()).eq in let sym = (build_coq_eqT_data ()).sym in let eq = applist (e, [t1;c1;c2]) in - tclTHENS (cut eq) - [tclTHEN intro (onLastHyp (fun id -> - tclTHEN (rewriteRL_clause clause (mkVar id,NoBindings)) (clear [id]))); + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN (rewriteRL_clause clause (mkVar id,NoBindings)) (clear [id])); tclORELSE assumption (tclTRY (tclTHEN (apply sym) assumption))] gl else |