coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)	jforest	2008-03-08
*	Backtrack changes on eauto, move specialized version of eauto in	msozeau	2008-02-14
*	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau	2008-02-09
*	Change implementation of resolution for typeclasses to use a customized	msozeau	2008-02-08
*	Work-in-progress to make eauto accept a list of goals as input and	msozeau	2008-02-06
*	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
*	Export de simplest_eapply, utilisé dans la contrib interface	notin	2007-04-16
*	Suite unification apply et eapply (l'un et l'autre profite maintenant	herbelin	2007-04-16
*	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin	2006-01-28
*	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin	2006-01-24
*	A la demande de Julien Forest	letouzey	2005-11-17
*	Nouvelle en-tête	herbelin	2004-07-16
*	Interface Eauto	herbelin	2003-09-18