coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Work on dependent induction tactic and friends, finish the test-suite example	msozeau	2008-01-30
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Add a new tactic to generalize an instantiated inductive predicate adding equ...	msozeau	2007-08-07
*	extension of the rename tactic: the following is now allowed:	letouzey	2007-07-06
*	A fix for bug #1397:	letouzey	2007-05-23
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	Essai de partage de code entre apply et eapply	herbelin	2007-04-15
*	Changement dans le kernel :	bgregoir	2006-12-11
*	Ajout de la tactique "apply in".	herbelin	2006-10-24
*	Correction du bug #1116	jforest	2006-07-20
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin	2006-05-30
*	adding a new tactic [intro_avoiding idl] which acts as intro but prevents the	jforest	2006-04-11
*	+ destruct now works as induction on multiple arguments :	jforest	2006-03-21
*	-Debugging multiple induction, a bug appeared when having function	courtieu	2006-03-12
*	changed the decomposition of an induction scheme	coq	2006-02-17
*	added isProd to term.mli.	coq	2006-02-16
*	induction now admits multiple induction arguments. The principle must	coq	2006-02-10
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin	2006-01-16
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Changement des named_context	gregoire	2005-12-02
*	Ajout de l'axiome du but prouve par la tactique simplifi	coq	2005-03-22
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin	2005-03-07
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin	2005-01-02
*	Restructuration fonctions de réécriture depuis égalité dépendante; facto...	herbelin	2004-10-27
*	reflexivity, symmetry, symmetry ... in e transitivity now fall-back	sacerdot	2004-10-14
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	unification encore...	barras	2004-09-08
*	Nouvelle en-tête	herbelin	2004-07-16
*	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin	2004-03-02
*	Correction sur commit précédent : Tactics.cut réduisait de manière inappr...	herbelin	2004-03-01
*	Déplacement définition intro_pattern_expr dans Genarg	herbelin	2004-03-01
*	bugs avec Pose et Assert	barras	2004-01-09
*	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin	2003-11-25
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Un type "standardisé" pour new_hyp	herbelin	2003-01-25
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin	2002-10-21
*	NewDestruct/NewInduction acceptent l'option "using"	herbelin	2002-10-21