coq - The formal proof system

Age	Commit message (Expand)	Author
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2005-12-05	changement d'egalite pour le named_context_val	gregoire
2005-12-02	Changement des named_context	gregoire
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-04	Confusion assert/error détectée par nouveau warning X de ocaml 3.09	herbelin
2005-10-27	catchable_exception laisse passer les InductiveError	werner
2005-07-13	Correction double bug #986: Fold ne préserve pas nécessairement le typage e...	herbelin
2005-05-28	unification: evar_define checks the free variables are bound in the evar context	barras
2005-05-20	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin
2005-05-15	Allow auto to have a parametric argument (wish #967)	herbelin
2005-04-29	Protection against saving a proof with still non-instantiated evars (cf bug #...	herbelin
2005-04-29	Protection against saving a proof with still non-instantiated evars (cf bug #...	herbelin
2005-04-20	Implementation of a new backtracking system, that allow to go back	coq
2005-03-19	Correction erreur grossière de non restauration d'état en cas de retour exc...	herbelin
2005-03-07	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin
2005-02-04	Ajout constructeur External pour appel outil externe à Coq	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	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-12-31	Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...	herbelin
2004-12-31	Suppression de la dépendance en Tacmach pour pouvoir être appelé de top_pr...	herbelin
2004-11-18	Code mort	herbelin
2004-11-17	Mise en page	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-10-11	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-10	simplification de clenv	barras
2004-09-10	When refining a given term, the primitive refiner used to accepts some casts,	sacerdot
2004-09-08	unification encore...	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	deplacement de clenv vers pretyping	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-07-13	bugs #667 and #783 (mimick_evar and loc_table on large files)	barras
2004-07-07	bypass w_Define when w_refine-ing	corbinea
2004-06-30	updated printing of evar context (may loop ?)	corbinea
2004-06-29	moved instantiate binding to extratactics	corbinea
2004-06-28	more evar stuff	corbinea
2004-06-26	effective evar refining	corbinea
2004-04-20	Amélioration message d'erreur quand échec unification	clrenard
2004-03-29	Export du type de preuve en cours pour xml	herbelin
2004-03-02	Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-01	Déplacement définition intro_pattern_expr dans Genarg	herbelin
2004-02-26	added breakpoints to help ide	corbinea
2004-02-12	Localisation des erreurs d'internalisation des notations de tactiques	herbelin
2004-01-09	bugs avec Pose et Assert	barras