diff options
| author | letouzey | 2012-05-22 12:09:18 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-22 12:09:18 +0000 |
| commit | d08282cb2242d642d8ea40e844dbe61b7404674c (patch) | |
| tree | d1a8aa04194ed5c9adae5ec923915e12c8de5b28 /plugins/xml | |
| parent | 7511435a39d70625cde2949ddcc70684525a87e9 (diff) | |
SetoidList: explicit the fact that InfA_compat won't use ltA_strorder
For that, we use the new "Proof using ...". This way, we're sure
that a later change in the behavior of intuition or any other tactics
will not create an artificial dependency again (cf. r15180).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15340 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml')
0 files changed, 0 insertions, 0 deletions