coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr	2000-12-12
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
*	Renommage canonique :	herbelin	2000-10-18
*	Abstraction de constr	herbelin	2000-09-14
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
*	modifs pour premiere edition de liens	filliatr	1999-12-02
*	- environment -> safe_environment	filliatr	1999-12-01
*	ajouts divers pour module Printer	filliatr	1999-11-26
*	typage des existentielles dans Typing_ev; suppression metamap inutiles dans t...	filliatr	1999-11-25
*	Backtrack sur modif Evd.evd_concl	herbelin	1999-11-25
*	MAJ pour fusion avec pretyping	herbelin	1999-11-24
*	- documentation repertoire proofs/	filliatr	1999-10-20
*	les variables existentielles contiennent maintenant un environnement (type	filliatr	1999-10-19
*	- déplacement (encore une fois !) des variables existentielles : elles sont	filliatr	1999-10-18
*	module Proof_trees	filliatr	1999-10-14
*	- re-introduction d'une evar_map dans unsafe_env	filliatr	1999-10-13
*	redeplacement des var. ex. dans kernel :-)	filliatr	1999-10-13
*	deplacements des var. ex. hors du noyau	filliatr	1999-10-08
*	environnement sur	filliatr	1999-08-26
*	modules Instantiate, Constant et Inductive	filliatr	1999-08-25
*	machine: execute = typage avec univers	filliatr	1999-08-20
*	mise en place programmation literaire (generation de doc/coq.tex)	filliatr	1999-08-19
*	generic, term et evd	filliatr	1999-08-17