coq - The formal proof system

Age	Commit message (Expand)	Author
2007-05-25	Modification of VernacScheme to handle a new scheme: Equality (equality in	vsiles
2007-05-24	fixed (PR#1483)	corbinea
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-17	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-29	Orthographe en passant	herbelin
2007-04-29	Ajout possibilité d'options à trois mots.	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-04-17	Correct implementation of undo in obligations handling code, correct some bug...	msozeau
2007-04-16	Export de simplest_eapply, utilisé dans la contrib interface	notin
2007-04-05	Mise en place d'une nouvelle strategie plus efficace pour les preuves de Func...	jforest
2007-04-02	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov
2007-03-28	Support for implicit formal argument types in Program ; parse types in type s...	msozeau
2007-03-26	Make multiple patterns work again with Program while simplifying the code.	msozeau
2007-03-20	Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...	msozeau
2007-03-20	traces Ergo	filliatr
2007-03-19	Forgot to update to new cast	msozeau
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-03-16	r11153@tannat: jforest \| 2007-03-16 10:25:55 +0100	jforest
2007-03-15	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin
2007-03-15	Add destruct_call variant where naming of introduced hypotheses is possible. ...	msozeau
2007-03-14	Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ...	msozeau
2007-03-13	Solve obligation handling bug of trying to solve automatically at Next Obliga...	msozeau
2007-03-11	correction du bug 1432	jforest
2007-03-11	Remove bugguy notations	msozeau
2007-03-08	Create a program_scope in subtac Utils	msozeau
2007-02-28	The right tactics for definitions using measures.	msozeau
2007-02-27	Fix wf bug from F. Besson and work on ineqs generation.	msozeau
2007-02-24	Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)	herbelin
2007-02-24	Opacity parameterization for obligations working.	msozeau
2007-02-23	Debug wellfounded defs, work on cleaning obls envs	msozeau
2007-02-22	Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #...	notin
2007-02-19	Correct coq depend, add eq_rect elimination tactic to SubtacTactics	msozeau
2007-02-19	Various little subtac fixes, add some useful tactics.	msozeau
2007-02-16	Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.	msozeau
2007-02-16	lift params appropriately, do not need to coerce to tycon	msozeau
2007-02-16	Update implementation for dependent types. Works just as well as before for s...	msozeau
2007-02-14	encodage des types	filliatr
2007-02-14	tactique yices	filliatr
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-12	Bug mineur dans la generation des principes d'induction pour Function	jforest
2007-02-12	Fix matching on dependent types, taking a safe stand.	msozeau
2007-02-11	Correction d'un bug dans la génération des principes d'induction	jforest
2007-02-09	Retour r9310 en attendant mieux	herbelin
2007-02-09	Separate Tactics in subtac.	msozeau
2007-02-08	Add lif then else for if in bool.	msozeau