From aba4b1924f562d861ab2cf7ec75c507f0efe0d1f Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 12 Dec 2009 20:46:07 +0000 Subject: 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 --- tactics/autorewrite.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/autorewrite.ml') 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::_ -> -- cgit v1.2.3