coq - The formal proof system

Age	Commit message (Expand)	Author
2008-10-18	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin
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-05-05	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin
2008-04-27	Quelques bricoles autour de l'unification:	herbelin
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-14	Diverses corrections	herbelin
2008-03-21	Correct bug introduced in r10589, where we lost information that	msozeau
2008-03-10	Pas très propre de reposer sur la capture des anomalies (et cela	herbelin
2008-03-10	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-09-26	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-06-06	Toujours l'unification de apply : nouveau raffinement pour ne tester	herbelin
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-23	Suite restructuration unification et division des problèmes	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-21	Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-02-21	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin
2007-01-22	Correction du bug #1315:	notin
2006-11-19	Raffinement de l'unification de "apply": mémorisation de certains	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-04-28	Standardisation du nom des méthodes de Evd	herbelin
2006-04-07	- Documentation of the Program tactics.	msozeau
2005-12-05	changement d'egalite pour le named_context_val	gregoire
2005-12-02	Changement des named_context	gregoire
2005-06-07	reparations de quelques petits bugs d\'unification + introduction de la notio...	barras
2005-03-08	Ajout fold	herbelin
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-10-20	COMMITED BYTECODE COMPILER	barras
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-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-06-30	updated printing of evar context (may loop ?)	corbinea
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2001-11-06	Suppression des local_constraints, des ctxtty et du focus.	clrenard
2001-11-05	GROS COMMIT:	barras