coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq's kernel reduction mechanism

From: Chantal Keller <chantal.keller AT wanadoo.fr>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Coq's kernel reduction mechanism
Date: Wed, 17 Oct 2012 17:28:26 +0200

Dear Coq club,

I am looking for information about the "standard" Coq's kernel reduction
mechanism. By this, I mean the mechanism involved in the conversion rule
when doing "Qed." (in usual proofs, ie. when the VM is not called). Can
you give me a pointer on its working?

Thanks,
--
Chantal KELLER

[Coq-Club] Coq's kernel reduction mechanism, Chantal Keller, 10/17/2012
- Re: [Coq-Club] Coq's kernel reduction mechanism, Maxime Dénès, 10/17/2012
  - Re: [Coq-Club] Coq's kernel reduction mechanism, Chantal Keller, 10/18/2012