|File Search||Catalog||Content Search|
This package provides existing theories from Coq 7 in Coq 8, and allows proofs that were developed in Coq 7 to be used in Coq 8. It is also required to translate theories in Coq 7 syntax into the new syntax introduced in Coq 8. However, this package does not need to be installed to use Coq 7.
coq (8.0pl3-2) unstable; urgency=low * Added coq-8.0pl3-ocaml-3.09.dpatch in order to prevent intuition from looping forever, closes: #353493. -- Samuel Mimram <email@example.com> Sun, 19 Feb 2006 11:33:21 +0000 coq (8.0pl3-1) unstable; urgency=low * New upstream release. * Removed unnecessary dependency on liblablgtk2-ocaml for coqide. * Removed ocaml309.dpatch and text_view_ty more»
Changes from V8.0pl2 to V8.0pl3 =============================== Tactics - The search depth argument of auto can be parameterised in the Ltac language - Added entry constr_may_eval for tactic extensions (new syntax) Compilation - Coq sources made compatible with ocaml 3.09.0 and lablgtk 2.6.0. Standard library - A couple of lemmas of ZArith were renamed. This concerns names containing O ( more»
This package was debianized by Fernando Sanchez <firstname.lastname@example.org> It was downloaded from ftp://ftp.inria.fr/INRIA/LogiCal/coq/current The Coq proof assistant V7 and V8 includes software developed by the Coq development team inside the LogiCal project, at INRIA, CNRS and University Paris Sud. Copyright 1999-2005 The Coq development team, INRIA-CNRS, University Paris Sud, All rights reserved. more»