coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Are discriminated hint databases useful?
- Date: Mon, 6 Mar 2017 17:15:39 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jacques-henri.jourdan AT normalesup.org; spf=Neutral smtp.mailfrom=jacques-henri.jourdan AT normalesup.org; spf=None smtp.helo=postmaster AT ulminfo.fr
- Ironport-phdr: 9a23:aAE0CBRXDEyDaRmlW5XJsygcEdpsv+yvbD5Q0YIujvd0So/mwa6yZRWN2/xhgRfzUJnB7Loc0qyN4v2mBTRLsc3JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanb75/KBW7oR/eu8UKjodvKag8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9DvhyvpwFxzY3abo6bO/VxYqzTcMgGRWdDRMtdSzBND42+YoYJEuEPPfxYr474p1YWqRWxHxWjBPryyjBWnX/6xK803PonEQHc3QwrAtYAsHPJrNXvKagdS+a1x7TPwDXBdfxZxS796JXWfRA6uP2MXax/cczLyUkuDQ/FjFKQqZH/PzyIzOsNtXOW7+xnVeK1jm4osQVxrSa0xscxkonFnIUVykrL9Shgxos+ON62SFZjbNOkCpdcqi+XOotsTs8/QGxluzw2xqAItJO/ZCQG1ZoqyhrFZ/Cad4WE+A/vWeeSLDtiin9ofLSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1wHX6siCS/t9+Emh2TGV2wDd8OFIOUE0lazFJJ492rM9loAfvVnNEyL2gkn6kaybe0Y+9uS15enqZq3qppqGOI91jgH+PL4umsu6AekgMAgBRXSU+f2h1LL95k31WbVKgeMwkqnDsZDWP8YbpqmkAw9Pz4ks8RC/Aiyg0NQfh3kHKUhKeBaZgIjyJlHOOOr0DfClg1SjiDtr3ezJPqX9ApXRKXjOiKvufbFk60JF1AUzyc1f6IlPB7EaIPPzX1fxu8bCAh84NQy02efnB89n2oMQQ2LcSpOeZajVqBqD4v8lC+iKfo4c/jjneNY/4Pu7r3YygEIQZuyJ0J0NaTiaGel8L0yfKS7ui9wYDGoR+wozSvbrzl+FTCRfbnCaWaUm4zg/BZm7FcHEXI/70+/J5zuyApADPjMOMVuLC3q9L4g=
Hi Coq-club,
It seems like the [discriminated] keyword that one can add when creating a hint database does not change either the behavior nor the performance of eauto, auto and typeclasses eauto.
Is this any useful for someone?
--
JH Jourdan
- [Coq-Club] Are discriminated hint databases useful?, Jacques-Henri Jourdan, 03/06/2017
Archive powered by MHonArc 2.6.18.