coq - The formal proof system

Age	Commit message (Expand)	Author
2007-07-06	extension of the rename tactic: the following is now allowed:	letouzey
2007-05-23	A fix for bug #1397:	letouzey
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-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-15	Essai de partage de code entre apply et eapply	herbelin
2006-12-11	Changement dans le kernel :	bgregoir
2006-10-24	Ajout de la tactique "apply in".	herbelin
2006-07-20	Correction du bug #1116	jforest
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-04-11	adding a new tactic [intro_avoiding idl] which acts as intro but prevents the	jforest
2006-03-21	+ destruct now works as induction on multiple arguments :	jforest
2006-03-12	-Debugging multiple induction, a bug appeared when having function	courtieu
2006-02-17	changed the decomposition of an induction scheme	coq
2006-02-16	added isProd to term.mli.	coq
2006-02-10	induction now admits multiple induction arguments. The principle must	coq
2006-01-16	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin
2006-01-16	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-03-22	Ajout de l'axiome du but prouve par la tactique simplifi	coq
2005-03-07	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2005-01-02	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin
2004-10-27	Restructuration fonctions de réécriture depuis égalité dépendante; facto...	herbelin
2004-10-14	reflexivity, symmetry, symmetry ... in e transitivity now fall-back	sacerdot
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-08	unification encore...	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-01	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-01-09	bugs avec Pose et Assert	barras
2003-11-25	Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...	herbelin
2003-11-13	factorisation et generalisation des clauses	barras
2003-10-13	Deplacement next_global_ident_away dans Termops	herbelin
2003-10-10	changement nouvelle syntaxe (pt fixes)	barras
2003-06-19	Ajout 'Symmetry in Hyp'	herbelin
2003-06-13	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-01-25	Un type "standardisé" pour new_hyp	herbelin
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-10-21	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin
2002-10-21	NewDestruct/NewInduction acceptent l'option "using"	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-04-11	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin
2002-03-27	Simplification de Proof_type.prim_rule	herbelin