coq - The formal proof system

Age	Commit message (Expand)	Author
2008-09-11	Add enough information to correctly globalize recursive calls in inductive and	msozeau
2008-09-07	Better handling of the opacity of proof obligations, add the possibility of	msozeau
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-24	Suite commit 11236	notin
2008-07-23	Stop glob messages to be printed by default on stdout	letouzey
2008-07-22	Correct implementation of discharging of implicit arguments and add new	msozeau
2008-07-22	Oubli lors du commit #11236	notin
2008-07-21	Suite commit 11236	notin
2008-07-18	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin
2008-07-18	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-07-15	Autour du parsing:	herbelin
2008-07-07	Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...	notin
2008-07-07	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau
2008-07-04	Fixes in handling of implicit arguments:	msozeau
2008-07-01	Documentation Prop<=Set et Arguments Scope Global	herbelin
2008-06-25	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin
2008-06-21	Code cleanup in typeclasses, remove dead and duplicated code.	msozeau
2008-06-14	Correction bug 1878 (utilisation de extend_evar déplacée là où une	herbelin
2008-06-08	- Extension de "generalize" en "generalize c as id at occs".	herbelin
2008-06-06	Enhancements to coqdoc, better globalization of sections and modules.	msozeau
2008-06-03	Fix setoid_rewrite documentation examples.	msozeau
2008-05-30	Improvements on coqdoc by adding more information into .glob	msozeau
2008-05-28	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin
2008-05-24	Ajout de la possibilité d'utiliser fix/cofix dans les notations.	herbelin
2008-05-12	Fix "not an applied typeclass" error for legitimate classes	msozeau
2008-05-10	- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des	herbelin
2008-05-07	Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757	herbelin
2008-05-06	Better parsing of typeclasses, any constr is allowed for ! bindings so	msozeau
2008-05-06	Postpone the search for the recursive argument index from the user given	msozeau
2008-05-04	Factorize code for internalization of binders to fix bug #1846. Also	msozeau
2008-04-14	Diverses corrections	herbelin
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2008-04-12	Add the ability to specify what to do with free variables in instance	msozeau
2008-04-09	Correction bug List.map2 dans Case12.v	herbelin
2008-04-04	Quelques améliorations des intro patterns:	herbelin
2008-04-02	Add the ability to specify the implicit status of section variables and	msozeau
2008-04-01	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin
2008-04-01	Enhance handling of parameters in typeclass constraints: permit to specify an...	msozeau
2008-03-31	- Fix for rewriting under dependent products.	msozeau
2008-03-30	Modifications diverses et variées :	herbelin
2008-03-30	Ajout d'abbréviations/notations paramétriques	herbelin
2008-03-28	- Second pass on implementation of let pattern. Parse "let ' par [as x]?	msozeau
2008-03-27	Various fixes on typeclasses:	msozeau
2008-03-24	Finish fix in command where we still lost information on what was a type	msozeau
2008-03-23	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau
2008-03-20	Add a flag to control rewriting under lambdas. Otherwise makes some	msozeau
2008-03-19	Do another pass on the typeclasses code. Correct globalization of class	msozeau
2008-03-15	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau
2008-02-08	Move generally useful definition of nf_evar on contexts to evarutil.	msozeau