coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A try at using sort variables during unification. Instead of refreshing	msozeau	2009-05-23
*	- Fixing bug #2084 (unification not checking sort constraints), hoping	herbelin	2009-04-08
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Backtrack sur la mémoïsation de nf_evar.	aspiwack	2009-03-04
*	=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...	aspiwack	2009-02-27
*	On passe les last_mods (un des champs de Evd.evar_defs) de list	aspiwack	2009-02-20
*	On remplace evar_map par evar_defs (seul evar_defs est désormais exporté	aspiwack	2009-02-19
*	Really compare evar maps in progress, due to merging in apply and other	msozeau	2009-01-23
*	DISCLAIMER	puech	2009-01-17
*	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin	2008-10-26
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	Better handling of the opacity of proof obligations, add the possibility of	msozeau	2008-09-07
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin	2008-05-05
*	Quelques bricoles autour de l'unification:	herbelin	2008-04-27
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	Diverses corrections	herbelin	2008-04-14
*	Correct bug introduced in r10589, where we lost information that	msozeau	2008-03-21
*	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	2008-03-10
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin	2007-09-26
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	Toujours l'unification de apply : nouveau raffinement pour ne tester	herbelin	2007-06-06
*	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin	2007-05-29
*	Contrôle de la compatibilité de apply via une information dans les	herbelin	2007-05-28
*	Suite restructuration unification et division des problèmes	herbelin	2007-05-23
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	Essai d'une nouvelle heuristique pour clenv_unique_resolver : si le	herbelin	2007-05-21
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin	2007-02-21
*	Correction du bug #1315:	notin	2007-01-22
*	Raffinement de l'unification de "apply": mémorisation de certains	herbelin	2006-11-19
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
*	- Documentation of the Program tactics.	msozeau	2006-04-07
*	changement d'egalite pour le named_context_val	gregoire	2005-12-05
*	Changement des named_context	gregoire	2005-12-02
*	reparations de quelques petits bugs d\'unification + introduction de la notio...	barras	2005-06-07
*	Ajout fold	herbelin	2005-03-08
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30