The Coq mailing list

[Arnaud Spiwack <arnaud AT spiwack.net>]

Side-tracking from the multicore thread:

Enrico Tassi wrote:

Well, a patch to make "Print Assumptions qualid" render all the
occurrences of "match daemon return P with end" as "Axiom foo_admitted$N :
P" is not that hard to write.

This sounds to me like piling a hack over a hack. Plus, do we really want to have "Axiom deamon : False" in the environment? I would personally feel a bit uncomfortable about that.

Wouldn't it be better to add, in Term.constr a constructor for admitted subterms? (I'm aware it would be quite a bit of a deal to modify Term.constr, though, but let's talk in principle). In any case, if you want to have an irreducible/opaque let-in for "abstract", you'll have to stick you hand into Term.constr, won't you?

--

'When I use a word,' Humpty Dumpty said in rather a scornful tone, 'it means just what I choose it to mean—neither more nor less.'

- Through the looking glass and what Alice found there, Lewis Caroll