diff options
| author | barras | 2004-09-27 12:32:02 +0000 |
|---|---|---|
| committer | barras | 2004-09-27 12:32:02 +0000 |
| commit | 8f19d3b52c91fc86796cf9572ada5ba7d653d3d5 (patch) | |
| tree | 367d266eb566679a505574f71ba92639605064cf | |
| parent | e1626554be06a5af1cd5761e27b4b3acbaca2cd8 (diff) | |
corrected bug when lhs is matched w.r.t delta
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6140 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/setoid_replace.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 418a545cd1..3b809fbb08 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1096,9 +1096,8 @@ let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h) let relation_rewrite c1 c2 (input_direction,cl) gl = let but = pf_concl gl in let (hyp,c1,c2) = - let cl' = - {cl with env = fst (w_unify_to_subterm (pf_env gl) (c1,but) cl.env)} in - let c1 = Clenv.clenv_nf_meta cl' c1 in + let (env',c1) = w_unify_to_subterm (pf_env gl) (c1,but) cl.env in + let cl' = {cl with env = env' } in let c2 = Clenv.clenv_nf_meta cl' c2 in (input_direction,Clenv.clenv_value cl'), c1, c2 in @@ -1146,8 +1145,9 @@ let temporary_solution2 prop_relation gl = (mkApp (th, [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl in (*CSC: the prop_relation will be returned by mark_occur *) - Tacticals.tclORELSE (temporary_solution (Lazy.force coq_prop_relation)) - (temporary_solution2 (Lazy.force coq_prop_relation2)) gl + Tacticals.tclFIRST + [temporary_solution (Lazy.force coq_prop_relation); + temporary_solution2 (Lazy.force coq_prop_relation2)] gl let general_s_rewrite lft2rgt c gl = let direction = if lft2rgt then Left2Right else Right2Left in |