diff options
| author | notin | 2007-03-30 13:00:00 +0000 |
|---|---|---|
| committer | notin | 2007-03-30 13:00:00 +0000 |
| commit | 7c8c9900b8c9eb20ba2db42fbe445c95e3aa149a (patch) | |
| tree | 90aba856d1937f8d135b547c23603ab902413e4d | |
| parent | bfba94a477393f87a9af8b3e37d15a776ffa4648 (diff) | |
Changement mineur du comportement de 'rewrite .. in * |-': si le
constr avec lequel on réécrit contient une hypothèse H, on ne réécrit
pas dans H (corrige le bug #1446)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9735 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/equality.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index e2b3ec57c2..f00cdcd00d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -144,14 +144,14 @@ let general_multi_rewrite l2r c cl = (do_hyps_atleastonce l) in let do_hyps gl = - (* If the term to rewrite is an hypothesis, don't rewrite in itself *) - let ids = match kind_of_term (fst c) with - | Var id -> list_remove id (pf_ids_of_hyps gl) - | _ -> pf_ids_of_hyps gl + (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) + let ids = + let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in + Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl) in do_hyps_atleastonce ids gl in - if not cl.onconcl then do_hyps - else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps + if not cl.onconcl then do_hyps + else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps (* Conditional rewriting, the success of a rewriting is related to the resolution of the conditions by a given tactic *) |