. Proof, Defined . Same as Proof . . . . Qed . but the proof is then declared transparent (see 5.2.5), which means it can be unfolded in conversion tactics

. Goal-type, Save ident Same as Lemma ident: type. . . Save. This is intended to be used in the interactive mode. Conversely to named lemmas, anonymous goals cannot be nested

<. Coq and . F_atom, index -> formula. (* constructor for variables *)

<. Coq and . Undo, Quote interp_f, subgoal ============================ (interp_f (Node_vm C<->C (Empty_vm Prop) (Empty_vm Prop)) (f_and (f_const A) (f_and (f_or (f_const A) f_true) (f_and (f_not (f_const B)) (f_atom End_idx)))))

. Omega, a solver of quantifier-free problems in Presburger Arithmetic 233

O. Description, 233 Arithmetical goals recognized by, p.234

.. Technical-data, 235 Overview of the tactic, OMEGA decision procedure, vol.235, p.235

W. How, 237 Syntax of annotated programs, p.238

G. Local, 243 Global variables, p.244

M. Generating and .. , 251 Preview within Coq toplevel, 252 Generating real Ocaml files 252 Generating real Haskell files, p.252

. Ph and . Audebaudens-lyon, CC+ : an extension of the Calculus of Constructions with fixpoints, Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp.21-34, 1992.

. Ph and . Audebaud, Extension du Calcul des Constructions par Points fixes, 1992.

L. Augustsson, Compiling pattern matching, Conference Functional Programming and Computer Architecture, 1985.
DOI : 10.1007/3-540-15975-4_48

H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, 1991.

H. P. Barendregt, The Lambda Calculus its Syntax and Semantics, 1981.

J. L. Bates and R. L. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems, vol.7, issue.1, 1985.
DOI : 10.1145/2363.2528

M. J. Beeson, Foundations of Constructive Mathematics, Metamathematical Studies, 1985.

G. Bellin and J. Ketonen, A decision procedure revisited: notes on direct logic, linear logic and its implementation, Theoretical Computer Science, vol.95, issue.1, pp.115-142, 1992.
DOI : 10.1016/0304-3975(92)90069-R

E. Bishop, Foundations of Constructive Analysis, 1967.

S. Boutin, Certification d'un compilateur ML en Coq, 1992.

S. Boutin, Réflexions sur les quotients. thèse d'université, 1997.

S. Boutin, Using reflection to build efficient and certified decision procedures, TACS'97, 1997.
DOI : 10.1007/BFb0014565

R. S. Boyer and J. S. Moore, A computational logic, 1979.

R. L. Constable, Implementing Mathematics with the Nuprl Proof Development System, 1986.

. Th and . Coquand, Une Théorie des Constructions, 1985.

. Th and . Coquand, An Analysis of Girard's Paradox, Symposium on Logic in Computer Science, 1986.

. Th and . Coquand, Metamathematical Investigations of a Calculus of Constructions, Logic and Computer Science, 1990.

. Th and . Coquand, Pattern Matching with Dependent Types

. Th and . Coquand, Infinite Objects in Type Theory, Barendregt and Nipkow

. Th, G. Coquand, and . Huet, Constructions : A Higher Order Proof System for Mechanizing Mathematics, EUROCAL'85, 1985.

. Th, G. Coquand, and . Huet, The Calculus of Constructions, Information and Computation, vol.76, issue.23, 1988.

. Th, C. Coquand, and . Paulin-mohring, Inductively defined types, Proceedings of Colog'88, 1990.

J. Courant, E. Informatique, and . Lyon, Explicitation de preuves par récurrence implicite, 1994.

N. J. De-bruijn, Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem, Indag. Math, vol.34, 1972.

N. J. De-bruijn, A Survey of the Project Automath, to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.
DOI : 10.1016/S0049-237X(08)70203-9

D. De-rauglaudre, Camlp4 version 1.07.2, Camlp4 distribution, 1998.

D. Delahaye, Information Retrieval in a Coq Proof Library Using Type Isomorphisms, Proceedings of TYPES'99, 1999.
DOI : 10.1017/S095679680000006X

]. D. Delahaye, A Tactic Language for the System Coq Reunion Island, Proceedings of Logic for Programming and Automated Reasoning (LPAR), pp.85-95, 2000.

D. Delahaye and M. Mayero, Field: une procédure de décision pour les nombres réels en Coq, 2001.

R. Di and C. , Isomorphisms of Types: from -calculus to information retrieval and language design, Progress in Theoretical Computer Science. Birkhauser, 1995.

G. Dowek, Naming and Scoping in a Mathematical Vernacular, Research Report, vol.1283, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00075276

G. Dowek, A second-order pattern matching algorithm for the cube of typed ??-calculi
DOI : 10.1007/3-540-54345-7_58
URL : https://hal.archives-ouvertes.fr/inria-00074975

G. Dowek, Démonstration automatique dans le Calcul des Constructions, 1991.

G. Dowek, Indécidabilité du Filtrage du Troisième Ordre dans les Calculs avec Types Dépendants ou Constructeurs de Types Compte Rendu de l'Académie des Sciences, I, pp.312951-956, 1991.

G. Dowek, The undecidability of pattern matching in calculi where primitive recursive functions are representable, Theoretical Computer Science, vol.107, issue.2, 1992.
DOI : 10.1016/0304-3975(93)90175-S

G. Dowek, A Complete Proof Synthesis Method for the Cube of Type Systems, Journal of Logic and Computation, vol.3, issue.3, pp.287-315, 1993.
DOI : 10.1093/logcom/3.3.287

G. Dowek, Third order matching is decidable, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.135-155, 1994.
DOI : 10.1109/LICS.1992.185514

G. Dowek, Lambda-calculus, Combinators and the Comprehension Schema, Proceedings of the second international conference on typed lambda calculus and applications, 1995.

G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy et al., The Coq Proof Assistant User's Guide Version 5, 1993.

P. Dybjer, Inductive sets and families in Martin-Löf's Type Theory and their set-theoretic semantics : An inversion principle for Martin-Löf's type theory, Logical Frameworks, pp.59-79, 1991.

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, 1992.
DOI : 10.1007/3-540-54487-9_58

J. Filliâtre, Une procédure de décision pour le Calcul des Prédicats Direct. Etude et implémentation dans le système Coq, 1994.

J. Filliâtre, A decision procedure for Direct Predicate Calculus, 1995.

J. Filliâtre, Preuve de programmes impératifs en théorie des types, Thèse de doctorat, 1999.

J. Filliâtre, Formal Proof of a Program: Find. Submitted to Science of Computer Programming, 2000.

J. Filliâtre, Verification of non-functional programs using interpretations in type theory, Journal of functional Programming, vol.13, issue.4, 2000.
DOI : 10.1017/S095679680200446X

J. Filliâtre and N. Magaud, Certification of sorting algorithms in the system Coq, Theorem Proving in Higher Order Logics: Emerging Trends, 1999.

E. Fleury, Implantation des algorithmes de Floyd et de Dijkstra dans le Calcul des Constructions, 1990.

P. Formel, The Calculus of Constructions. Documentation and user's guide, Version 4.10, 1989.
URL : https://hal.archives-ouvertes.fr/inria-00070056

J. Fourier, Fourier's method to solve linear inequations/equations systems, 1890.

E. and G. Lyon, Codifying guarded definitions with recursive schemes In Types'94 : Types for Proofs and Programs Extended version in LIP research report, LNCS, vol.996, pp.95-102, 1994.

E. Giménez, An application of co-inductive types in Coq: Verification of the alternating bit protocol, Workshop on Types for Proofs and Programs, number 1158 in LNCS, pp.135-152, 1995.
DOI : 10.1007/3-540-61780-9_67

E. Giménez, A tutorial on recursive types in coq, 1998.

J. Girard, Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types, Proceedings of the 2nd Scandinavian Logic Symposium. North-Holland, 1970.

J. Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972.

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7, 1989.

J. Harrison, Metatheory and reflection in theorem proving: A survey and critique, 1995.

D. Hirschkoff, Ecriture d'une tactique arithmétique pour le système Coq, 1994.

W. A. Howard, The formulae-as-types notion of constructions, to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.

G. Huet, Induction principles formalized in the calculus of constructions, Programming of Future Generation Computers Also in Proceedings of TAPSOFT87, pp.276-286, 1987.
DOI : 10.1007/3-540-17660-8_62

G. Huet, The Constructive Engine A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney, 1989.

G. Huet, The Gallina specification language: A case study, Proceedings of 12th FST/TCS Conference, pp.229-240, 1992.
DOI : 10.1007/3-540-56287-7_108

G. Huet, Abstract, Journal of Functional Programming, vol.34, issue.03, pp.371-394, 1994.
DOI : 10.1017/S0956796800001106

G. Huet and J. Lévy, Call by need computations in non-ambigous linear term rewriting systems, Computational Logic, Essays in Honor of Alan Robinson, 1979.

J. Ketonen and R. Weyhrauch, A decidable fragment of predicate calculus, Theoretical Computer Science, vol.32, issue.3, pp.297-307, 1984.
DOI : 10.1016/0304-3975(84)90047-1

S. C. Kleene, Introduction to Metamathematics, Bibliotheca Mathematica. North-Holland, 1952.

J. Krivine, Lambda-calcul types et modèles. Etudes et recherche en informatique, 1990.
DOI : 10.1051/ita/1991250100671
URL : http://archive.numdam.org/article/ITA_1991__25_1_67_0.pdf

A. Laville, Comparison of priority rules in pattern matching and term rewriting, Journal of Symbolic Computation, vol.11, issue.4, pp.321-347, 1991.
DOI : 10.1016/S0747-7171(08)80109-5
URL : https://hal.archives-ouvertes.fr/inria-00075676

F. Leclerc and C. Paulin-mohring, Programming with streams in Coq a case study: The Sieve of Eratosthenes, Types for Proofs and Programs, Types' 93, 1994.
DOI : 10.1007/3-540-58085-9_77

X. Leroy, The ZINC experiment: an economical implementation of the ML language, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

L. Puel and A. Suárez, Compiling Pattern Matching by Term Decomposition, Conference Lisp and Functional Programming, 1990.
DOI : 10.1006/jsco.1993.1001
URL : http://doi.org/10.1006/jsco.1993.1001

P. Manoury, A user's friendly syntax to define recursive functions as typed ??-terms, Types for Proofs and Programs, TYPES'94, 1994.
DOI : 10.1007/3-540-60579-7_5

P. Manoury and M. Simonot, Automatizing termination proofs of recursively defined functions, Theoretical Computer Science, vol.135, issue.2
DOI : 10.1016/0304-3975(94)00021-2
URL : https://hal.archives-ouvertes.fr/hal-00528475

L. Maranget, Two Techniques for Compiling Lazy Pattern Matching, 1994.
URL : https://hal.archives-ouvertes.fr/inria-00074292

C. Muñoz, Démonstration automatique dans la logique propositionnelle intuitionniste. Master's thesis, DEA d'Informatique Fondamentale, 1994.

C. Muñoz, Un calcul de substitutions pour la représentation de preuves partielles en théorie de types, Thèse de doctorat, 1997.

B. Nordström, Terminating general recursion, BIT, vol.24, issue.3, 1988.
DOI : 10.1007/BF01941137

B. Nordström, K. Peterson, and J. Smith, Programming in Martin-Löf's Type Theory. International Series of Monographs on Computer Science, 1990.

P. Martin-löf, Intuitionistic Type Theory, 1984.

C. Parent, Developing certified programs in the system Coq the program tactic, 1993.
DOI : 10.1007/3-540-58085-9_81

C. Parent, Synthèse de preuves de programmes dans le Calcul des Constructions Inductives, 1995.

C. Parent, Synthesizing proofs from programs in the Calculus of Inductive Constructions, Mathematics of Program Construction'95, 1995.
DOI : 10.1007/3-540-60117-1_20

M. Parigot, Recursive programming with proofs, Theoretical Computer Science, vol.94, issue.2, pp.335-356, 1992.
DOI : 10.1016/0304-3975(92)90042-E

M. Parigot, P. Manoury, and M. Simonot, ProPre : A Programming language with proofs, Logic Programming and automated reasoning, number 624 in LNCS, 1992.

C. Paulin-mohring, Extracting ??'s programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89
DOI : 10.1145/75277.75285

C. Paulin-mohring, Extraction de programmes dans le Calcul des Constructions, 1989.
URL : https://hal.archives-ouvertes.fr/tel-00431825

C. Paulin-mohring and . Lyon, Inductive definitions in the system Coq rules and properties, Proceedings of the conference Typed Lambda Calculi and Applications, number 664 in LNCS, 1993.
DOI : 10.1007/BFb0037116

C. Paulin-mohring, Le système Coq. Thèse d'habilitation, ENS Lyon, 1997.

C. Paulin-mohring and B. Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, vol.15, issue.5-6, pp.607-640, 1993.
DOI : 10.1016/S0747-7171(06)80007-6

K. V. Prasad, Programming with broadcasts, Proceedings of CONCUR'93, 1993.
DOI : 10.1007/3-540-57208-2_13

J. Rouyer, Développement de l'Algorithme d'Unification dans le Calcul des Constructions, 1992.

A. Saïbi, Axiomatization of a lambda-calculus with explicit-substitutions in the Coq System, 1994.

H. Saidi, Résolution d'équations dans le système t de gödel. Master's thesis, DEA d'Informatique Fondamentale, 1994.

D. Terrasse, Traduction de TYPOL en COQ. Application à Mini ML. Master's thesis, IARFA, 1992.

L. Théry, Y. Bertot, and G. Kahn, Real theorem provers deserve real user-interfaces, Research Report, vol.1684, 1992.

A. S. Troelstra and D. Van-dalen, Constructivism in Mathematics, an introduction, Studies in Logic and the foundations of Mathematics, volumes 121 and 123, 1988.

P. Wadler, Efficient compilation of pattern matching The Implementation of Functional Programming Languages, 1987.

B. Werner, Index of Error Messages Unité de recherche INRIA Rocquencourt Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche INRIA Lorraine : LORIA, Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38330 Montbonnot-St, Une théorie des constructions inductives Thèse de doctorat, pp.93-06902, 1994.