diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-12 20:46:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-12 20:46:07 +0000 |
| commit | aba4b1924f562d861ab2cf7ec75c507f0efe0d1f (patch) | |
| tree | 67199755041372c7f3dc6f7757795d9c0932fe9a /tactics/autorewrite.ml | |
| parent | c94207ce53c82652e2b5841da55cd5de5266445d (diff) | |
Updated compatibility for rewriting equality proofs that are dependent
- made the new "subst'" the default by renaming it "subst";
- renamed old "subst" into "simple subst";
- add option for non-rewriting of dependent proofs in general_rewrite and co
- kept use of dependent proofs in the "subst" call of "functional
induction", in spite it introduced incompatibilities (in Compcert).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12578 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 0b69eebbd..8495b623f 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -119,7 +119,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 ~tac c) + general_rewrite dir all_occurrences false ~tac c) tac_main bas)) tclIDTAC lbas)) @@ -137,7 +137,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) !id cstr false gl in + let gl' = general_rewrite_in dir all_occurrences ~tac:(tac, conds) false !id cstr false gl in let gls = (fst gl').Evd.it in match gls with g::_ -> |