diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-23 14:00:25 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-23 14:00:25 +0000 |
| commit | a2c939025a746eafb05e644fc887a4d54b6a34c6 (patch) | |
| tree | 7dc62732a9ba5a13f04bf731dcdd37a9dd79f4ba /tactics/tactics.mli | |
| 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/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 0c2024162..8de249867 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -290,16 +290,19 @@ val simplest_split : tactic (*s Logical connective tactics. *) val register_setoid_reflexivity : tactic -> unit +val reflexivity_red : bool -> tactic val reflexivity : tactic val intros_reflexivity : tactic val register_setoid_symmetry : tactic -> unit +val symmetry_red : bool -> tactic val symmetry : tactic val register_setoid_symmetry_in : (identifier -> tactic) -> unit val symmetry_in : identifier -> tactic val intros_symmetry : clause -> tactic val register_setoid_transitivity : (constr -> tactic) -> unit +val transitivity_red : bool -> constr -> tactic val transitivity : constr -> tactic val intros_transitivity : constr -> tactic |