coq - The formal proof system

Age	Commit message (Expand)	Author
2009-12-21	Generic support for open terms in tactics	herbelin
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-18	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin
2008-04-27	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin
2008-04-26	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2008-04-04	Protection de rewrite in contre le dépliage des constantes dans w_unify, ce qui	herbelin
2008-03-19	Do another pass on the typeclasses code. Correct globalization of class	msozeau
2008-02-09	Solde de code mort et petites optimisations sur lesquels je suis	herbelin
2008-02-07	Mise en place d'une toute petite amélioration de l'unification de	herbelin
2007-10-12	Uniformisation du comportement de rewrite et rewrite in : quand le	herbelin
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-02-22	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin
2006-10-25	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin
2006-10-24	Ajout de la tactique "apply in".	herbelin
2005-12-17	Orthographe de 'instantiate'	herbelin
2005-05-24	Added clenv_environments_evars that behaves as clen_environments but	sacerdot
2005-05-19	A wish by Bas Spitters granted: a little more of unification up to	sacerdot
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2004-11-16	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-10	simplification de clenv	barras
2004-09-08	unification encore...	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	deplacement de clenv vers pretyping	barras