diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-18 20:35:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-18 20:35:32 +0000 |
| commit | 32e18eb2ec0d44e4265f44d2f3f51daa7d67e9c0 (patch) | |
| tree | 7571347858ea69b085ba522ccebf78301b8c1ae1 /tactics/autorewrite.ml | |
| parent | 9d7499dcd4440aca458cb190ed108ae9b3adff17 (diff) | |
Relaxed the constraint introduced in r14190 that froze the existing
evars when rewriting. Use it for autorewrite and subst. Accept evars
instantiation in multi_rewrite so that rewrite alone remains
compatible (it is used in contribs, e.g. Godel, in places where it
does not seem absurd to allow it), but there are no good reason for
it. Comments welcome.
+ addition of some tests for rewriting (one being related to commit 14217)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14222 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 55e23d342..8ccf751c4 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -117,7 +117,7 @@ let autorewrite ?(conds=Naive) tac_main lbas = tclTHEN tac (one_base (fun dir c tac -> let tac = tac, conds in - general_rewrite dir all_occurrences false ~tac c) + general_rewrite dir all_occurrences true false ~tac c) tac_main bas)) tclIDTAC lbas)) @@ -135,7 +135,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic = | _ -> (* even the hypothesis id is missing *) error ("No such hypothesis: " ^ (string_of_id !id) ^".") in - let gl' = general_rewrite_in dir all_occurrences ~tac:(tac, conds) false !id cstr false gl in + let gl' = general_rewrite_in dir all_occurrences true ~tac:(tac, conds) false !id cstr false gl in let gls = gl'.Evd.it in match gls with g::_ -> |