diff options
| author | herbelin | 2009-12-13 15:02:23 +0000 |
|---|---|---|
| committer | herbelin | 2009-12-13 15:02:23 +0000 |
| commit | 2fb41f7561ead2abcff2ca31ccd3b1c88603c370 (patch) | |
| tree | dbc8c7a614b7a47e51c2db84cf5dfbd4bb2732f1 /tactics | |
| parent | 563d9e1066c7f6f0fb0263101013b015b3faa0bd (diff) | |
Revision 12557 continued (better rendering of dependent rewrite)
(expected goal was not correct for rewriting in hypotheses)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12580 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index c5ffe72b4d..b0570215ac 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1096,16 +1096,14 @@ let swapEquandsInConcl gls = (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *) -let bareRevSubstInConcl lbeq body expected_goal (t,e1,e2) gls = +let bareRevSubstInConcl lbeq body (t,e1,e2) gls = (* find substitution scheme *) let eq_elim = find_elim lbeq.eq (Some false) false None [e1;e2] gls in (* build substitution predicate *) let p = lambda_create (pf_env gls) (t,body) in (* apply substitution scheme *) - refine (applist(eq_elim, - [t;e1;p; - mkCast(Evarutil.mk_new_meta(),DEFAULTcast,expected_goal); - e2;Evarutil.mk_new_meta()])) gls + refine (applist(eq_elim,[t;e1;p;Evarutil.mk_new_meta(); + e2;Evarutil.mk_new_meta()])) gls (* [subst_tuple_term dep_pair B] @@ -1173,7 +1171,9 @@ let cutSubstInConcl_RL eqn gls = let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gls eqn in let body,expected_goal = pf_apply subst_tuple_term gls e2 e1 (pf_concl gls) in if not (dependent (mkRel 1) body) then raise NothingToRewrite; - bareRevSubstInConcl lbeq body expected_goal eq gls + tclTHENFIRST + (bareRevSubstInConcl lbeq body eq) + (convert_concl expected_goal DEFAULTcast) gls (* |- (P e1) BY CutSubstInConcl_LR (eq T e1 e2) @@ -1192,8 +1192,8 @@ let cutSubstInHyp_LR eqn id gls = let idtyp = pf_get_hyp_typ gls id in let body,expected_goal = pf_apply subst_tuple_term gls e1 e2 idtyp in if not (dependent (mkRel 1) body) then raise NothingToRewrite; - cut_replacing id (subst1 e2 body) - (tclTHENFIRST (bareRevSubstInConcl lbeq body expected_goal eq)) gls + cut_replacing id expected_goal + (tclTHENFIRST (bareRevSubstInConcl lbeq body eq)) gls let cutSubstInHyp_RL eqn id gls = (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id) |