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 | |
| 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
| -rw-r--r-- | contrib/ring/ring.ml | 4 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 19 | ||||
| -rw-r--r-- | tactics/setoid_replace.mli | 3 |
4 files changed, 25 insertions, 9 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index d72ee19e2c..2f42af6b71 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -806,8 +806,8 @@ let raw_polynom th op lc gl = c'''i; ci; c'i_eq_c''i |])))) (tclTHEN (tclORELSE - (Setoid_replace.setoid_replace ci c'''i ~new_goals:[]) - (Setoid_replace.setoid_replace c'''i ci ~new_goals:[])) + (Setoid_replace.setoid_replace None ci c'''i ~new_goals:[]) + (Setoid_replace.setoid_replace None c'''i ci ~new_goals:[])) (tclTHEN (tclTRY (h_exact c'i_eq_c''i)) tac))) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 93af58b5a6..1457f09daa 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -166,9 +166,13 @@ open Setoid_replace TACTIC EXTEND SetoidReplace [ "Setoid_replace" constr(c1) "with" constr(c2) ] -> - [ setoid_replace c1 c2 ~new_goals:[] ] + [ setoid_replace None c1 c2 ~new_goals:[] ] + | [ "Setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel)] -> + [ setoid_replace (Some rel) c1 c2 ~new_goals:[] ] | [ "Setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) ] -> - [ setoid_replace c1 c2 ~new_goals:l ] + [ setoid_replace None c1 c2 ~new_goals:l ] + | [ "Setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] -> + [ setoid_replace (Some rel) c1 c2 ~new_goals:l ] END TACTIC EXTEND SetoidRewrite 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 diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 5e08ffeaab..0a8405d039 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -23,7 +23,8 @@ val print_setoids : unit -> unit val equiv_list : unit -> constr list -val setoid_replace : constr -> constr -> new_goals:constr list -> tactic +val setoid_replace : + constr option -> constr -> constr -> new_goals:constr list -> tactic val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic |