diff options
| author | letouzey | 2007-05-23 14:00:25 +0000 |
|---|---|---|
| committer | letouzey | 2007-05-23 14:00:25 +0000 |
| commit | a2c939025a746eafb05e644fc887a4d54b6a34c6 (patch) | |
| tree | 7dc62732a9ba5a13f04bf731dcdd37a9dd79f4ba /tactics/setoid_replace.ml | |
| parent | b483e1732682bd1b8cec8d5d3a600c93d90f44ab (diff) | |
A fix for bug #1397:
setoid_reflexivity may discover it is doing plain Leibniz stuff (see
exception Optimize in setoid_replace), and falls back to the usual
reflexivity. Except that this one, due to the lack of delta-red,
refuses to handle the job, and gives it back to setoid_reflexivity:
a loop is born.
quick fix for the moment: add some whd_betadeltaiota to reflexivity in
the special situation where reflexivity is called back by
setoid_reflexivity.
Similar issue & fix for symmetry, transitivity.
rewrite has potentially the same problem, but I can't manage to trigger
a wild loop in practice. This code clearly deserves a closer look
someday...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 1e70bf2771..c66a55d38c 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1934,7 +1934,7 @@ let setoid_reflexivity gl = (str "The relation " ++ prrelation rel ++ str " is not reflexive.") | Some refl -> apply refl gl with - Optimize -> reflexivity gl + Optimize -> reflexivity_red true gl let setoid_symmetry gl = try @@ -1950,7 +1950,7 @@ let setoid_symmetry gl = (str "The relation " ++ prrelation rel ++ str " is not symmetric.") | Some sym -> apply sym gl with - Optimize -> symmetry gl + Optimize -> symmetry_red true gl let setoid_symmetry_in id gl = let new_hyp = @@ -1985,7 +1985,7 @@ let setoid_transitivity c gl = apply_with_bindings (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl with - Optimize -> transitivity c gl + Optimize -> transitivity_red true c gl ;; Tactics.register_setoid_reflexivity setoid_reflexivity;; |