Skip to Main content Skip to Navigation

A Small Scale Reflection Extension for the Coq system

Georges Gonthier 1 Assia Mahboubi 1, 2, 3, * Enrico Tassi 1, 2, 3
* Corresponding author
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : This is the user manual of Ssreflect, a set of extensions to the proof scripting language of the Coq proof assistant. While these extensions were developed to support a particular proof methodology - small-scale reflection - most of them actually are of a quite general nature, improving the functionality of Coq in basic areas such as script layout and structuring, proof context management, and rewriting. Consequently, and in spite of the title of this document, most of the extensions described here should be of interest for all Coq users, whether they embrace small-scale reflection or not.
Document type :
Complete list of metadatas
Contributor : Assia Mahboubi <>
Submitted on : Tuesday, March 11, 2014 - 5:11:53 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Document(s) archivé(s) le : Wednesday, June 11, 2014 - 1:11:46 PM


Files produced by the author(s)


  • HAL Id : inria-00258384, version 14


Georges Gonthier, Assia Mahboubi, Enrico Tassi. A Small Scale Reflection Extension for the Coq system. [Research Report] RR-6455, 2008. ⟨inria-00258384v14⟩



Record views


Files downloads