coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Core Verifier of Coq

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Core Verifier of Coq
Date: Thu, 12 Sep 2013 11:56:57 +0200

On Sun, Sep 08, 2013 at 11:31:53AM +0000, t x wrote:
> I'm not looking for unification / inference / notation / ltac. Nor am I
> interested in various proofs -- just the very core "dumb/minimal" verifier
> that verifiers the terms generated.

Maybe you should look at the checker/ directory. It is a standalone,
almost self contained, utility that "parses" .vo files and check the
proof terms. IIRC the make file target "check" runs it on the standard
library.

Cheers
--
Enrico Tassi

[Coq-Club] Core Verifier of Coq, t x, 09/08/2013
- Re: [Coq-Club] Core Verifier of Coq, Gabriel Scherer, 09/08/2013
  - Re: [Coq-Club] Core Verifier of Coq, Arnaud Spiwack, 09/09/2013
- Re: [Coq-Club] Core Verifier of Coq, Enrico Tassi, 09/12/2013