The Coq mailing list

[Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>]

Hello,

I have an installation of coq 8.1, coqide, and ocaml 3.0.9.2  in Ubuntu that I did
by using the deb packages. My question is would program extraction
work with this version, or do I need to install Coq from sources (including
sources).

Many thanks
Ashish

---

From: Razvan Voicu <razvan AT comp.nus.edu.sg>
To: Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>
Cc: coq-club AT pauillac.inria.fr
Sent: Wednesday, 29 October, 2008 4:46:15
Subject: RE: [Coq-Club] Guide to Coq Sources


Dear Jean-Francois,

Thanks for your pointer. It would certainly help with moving faster through
the code-base.

Regards,

Razvan

-----Original Message-----
From: coq-club-admin AT pauillac.inria.fr
[mailto:coq-club-admin AT pauillac.inria.fr] On Behalf Of Jean-Francois Monin
Sent: Friday, October 24, 2008 8:07 PM
To: Razvan Voicu
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Guide to Coq Sources

Hi,

This was our rationale to create otags, a fews year ago (joined work with
Cuithlauac Alvarado, who had the same problem).  Otags in now maintained by
Hendrik Tews and packaged in linux distros (Debian Ubuntu at least).

Of course it is far from a semantic answer.

Hope this may help anyway.

  JF

On Fri, Oct 24, 2008 at 06:24:41PM +0800, Razvan Voicu wrote:
> Hi,
> 
> I would like to implement a tactic that performs actions in a manner
> that is dependent on the shape of the partial proof of the current
> goal. From what I gather, this can only be done on Ocaml, since LTac
> makes no provisions for accessing the proof term. So, is there a guide
> to the Coq source tree? Or, could anyone provide some useful pointers?
> I would be particularly interested the source files containing the
> type that implements proof terms and the procedures that manipulate such
terms.
> 
> Thanks in advance,
> 
> Razvan
> 

--
Jean-Francois Monin          Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation    http://www-verimag.imag.fr/~monin/
2 avenue de Vignate          tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club