coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin	2007-04-18
*	Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,	herbelin	2007-04-14
*	Correction bug #1491	herbelin	2007-04-13
*	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin	2007-04-13
*	Modification de la vm:	notin	2007-03-27
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin	2007-03-15
*	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin	2007-02-22
*	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin	2007-02-21
*	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin	2007-02-21
*	Add functionality to permit printing terms with references to anonymous varia...	msozeau	2007-02-16
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Correction d'un bug dans check_and_clear_in_constr + simplification de	notin	2007-01-31
*	Nouvelle implantation de clear_hyps	notin	2007-01-30
*	correction d'un bug d'efficacite dans le printer	jforest	2007-01-26
*	Correction du bug #1315:	notin	2007-01-22
*	Correction d'un bug d'unification-pattern dans l'algo d'unification	herbelin	2007-01-22
*	Correction pour le rapport de bug #1325 par rétablissement du	herbelin	2007-01-22
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	Rework subtac pattern matching equalities generation.	msozeau	2007-01-02
*	Protection contre une source possible de liaison de lambda anonyme	herbelin	2006-12-29
*	Confusion sur le paramètre à donner à concrete_name lors du commit 9450	herbelin	2006-12-14
*	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin	2006-12-13
*	Correction du bug #1273, deuxième version (avec des shémas d'elimination pl...	notin	2006-12-12
*	Correction du bug #1273 (problème avec les paramètres non récursivement un...	notin	2006-12-12
*	Backtrack sur suppression des vars anonymes des contextes d'evars (echec Case...	herbelin	2006-12-12
*	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin	2006-12-12
*	Évitement des noms de constructeurs dans les motifs de filtrage de "match"	herbelin	2006-12-09
*	correction du bug : VM value extraction error (PR#1290)	bgregoir	2006-11-29
*	Code mort découvert par Matthieu	herbelin	2006-11-22
*	Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après	herbelin	2006-11-19
*	Raffinement de l'unification de "apply": mémorisation de certains	herbelin	2006-11-19
*	Code mort (duplication de code dans reductionops.ml)	herbelin	2006-11-18
*	Suppression source de complexité polynomiale introduite par le polymorphisme	herbelin	2006-11-03
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin	2006-10-25
*	Suite commit 9277	herbelin	2006-10-25
*	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin	2006-10-25
*	Ajout de la tactique "apply in".	herbelin	2006-10-24
*	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin	2006-10-21
*	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin	2006-10-21
*	Notations:	herbelin	2006-10-09
*	Remplacement des nf_evar (source de complexité polynomiale) par de la	herbelin	2006-10-06
*	Déplacement de on_judgment_type de Typeops vers Termops	herbelin	2006-10-06
*	Suppression d'une source de complexité polynomiale dans le pretypage	herbelin	2006-10-06
*	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin	2006-10-05
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
*	Ajout allowed_sorts	herbelin	2006-10-01