coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Michael Shulman <shulman AT sandiego.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] "default interpretation"
Date: Wed, 18 Nov 2015 09:14:55 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=viritrilbia AT gmail.com; spf=Pass smtp.mailfrom=viritrilbia AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f50.google.com
Ironport-phdr: 9a23:Ku/+KRc2m5qqxpZ45qGRemdqlGMj4u6mDksu8pMizoh2WeGdxc69Zh7h7PlgxGXEQZ/co6odzbGG7ua+ACdRut6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvcOKKFQTzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzazXwFGk4SjxAAVwPC9VTxWor7mir8rOt0nieAa57YV7cxDBGj5KdiRRugsycaMzsw9imDkcxtiKdSpjq6rhpzwoPbZ8eYOOcoLfCVRs8TWWcUBpUZbCdGGI7pKtJXV+c=

What does the parenthetical "(default interpretation)" mean when it
occurs in the output of "Locate"?

[Coq-Club] "default interpretation", Michael Shulman, 11/18/2015
- Re: [Coq-Club] "default interpretation", Jason Gross, 11/18/2015