diff options
| author | sacerdot | 2004-09-30 11:39:17 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-30 11:39:17 +0000 |
| commit | d723362607c3746944f2a67ecc58601b2ab64be3 (patch) | |
| tree | 6caa1686fe5d44c116d652efe9692fdccdc4f263 /tactics/setoid_replace.ml | |
| parent | f208cfc23dc997fd0409a9309628bc1804287d7d (diff) | |
cutrewrite does not work with relations that are not Coq-like equalities.
Thus it does not work for setoid relations and it can replace setoid_replace
when the user wants to specify what the relation should be.
To solve the problem this commit enables the syntax
setoid_replace E1 with E2 using relation R ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6163 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 7e22f8e5ee..aeae8040bf 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1342,12 +1342,23 @@ let general_s_rewrite lft2rgt c ~new_goals gl = exception Use_replace (*CSC: still setoid in the name *) -let setoid_replace c1 c2 ~new_goals gl = +let setoid_replace relation c1 c2 ~new_goals gl = try let relation = - match default_relation_for_carrier (pf_type_of gl c1) with - Relation sa -> sa - | Leibniz _ -> raise Use_replace + match relation with + Some rel -> + (try + match find_relation_class rel with + Relation sa -> sa + | Leibniz _ -> raise Use_replace + with + Not_found -> + errorlabstrm "Setoid_rewrite" + (prterm rel ++ str " is not a setoid equality.")) + | None -> + match default_relation_for_carrier (pf_type_of gl c1) with + Relation sa -> sa + | Leibniz _ -> raise Use_replace in let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in |