The Coq Proof Assistant : Reference Manual : Version 7.2

Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It helps to find formal proofs, and allows extraction of a certified program from the constructive proof of its formal specification. This document is the reference manual for the version V7.2 of Coq which is available from http://coq.inria.fr.

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/inria-00069919
Author Coq, The
Maintainer CCSD
Last Updated May 18, 2026, 02:42 (UTC)
Created May 18, 2026, 02:42 (UTC)
Identifier Report N°: RT-0255
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Logic and computing (LOGICAL) ; Université Paris-Sud - Paris 11 (UP11)-Centre Inria de Saclay ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-École polytechnique (X) ; Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)
creator Coq, The
date 2002-02-18T00:00:00
harvest_object_id 7a8aff40-f3ed-4c9b-ac5f-d3b192782b8c
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-08-20T00:00:00
set_spec type:REPORT