coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau	2008-10-23
*	Optimisation de clenv.ml pour que meta_instance ne soit pas appelé	herbelin	2008-10-18
*	Various little improvements:	msozeau	2008-09-25
*	Add a type argument to letin_tac instead of using casts and recomputing	msozeau	2008-09-12
*	Fix bug #1935, reworking the reflexivity, symmetry... tactics to use	msozeau	2008-09-03
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Fixes in generalize_eqs/dependent induction to allow the user to specify	msozeau	2008-07-28
*	New tactics [conv] to test convertibility (actually, unification) of two	msozeau	2008-07-22
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Quelques améliorations des intro patterns:	herbelin	2008-04-04
*	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin	2008-04-01
*	Added a function to rebuild an elim scheme from elim_scheme_info. Will	courtieu	2008-03-18
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	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