aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2006-03-05New files for subtaccoq
2006-03-05Renommage du IP classique pour éviter confusion avec IP constructifherbelin
2006-03-05Ajout étude IP généralisé, Gödel-Dummett, buveurherbelin
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...herbelin
2006-03-05Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...herbelin
2006-03-05Ajout test relatif au bug #984herbelin
2006-03-04Correction message d'erreur ltac et adoption du modèle de message de Tacinterpherbelin
2006-03-04majcoq
2006-03-04Petite simplification en passantherbelin
2006-03-04Titres moins envahissants pour coqdocherbelin
2006-03-03majcoq
2006-03-02majcoq
2006-03-02Correction bug #1097 (dû à une typo...)herbelin
2006-03-02Ajout test bug 1089herbelin
2006-03-02Correctif pour bug #1089 (cannot define an isevar twice)herbelin
2006-03-02tactic haRVey pour appeler haRVey (contrib/dp)filliatr
2006-03-02Correction du bug 808: il est maintenant interdit de déclarer une assomption...coq
2006-03-01Correction bug #842 (rename d'une hyp du contexte)herbelin
2006-03-01appel de Zenonfilliatr
2006-02-28majcoq
2006-02-28*** empty log message ***filliatr
2006-02-27majcoq
2006-02-27quelques raccourcis commodes + un f_equal plus efficaceletouzey
2006-02-27dp: sortie Whyfilliatr
2006-02-26majcoq
2006-02-25majcoq
2006-02-25changement de path du site webnarboux
2006-02-25ajoute un warning sur htmlppnarboux
2006-02-24majcoq
2006-02-23majcoq
2006-02-23trying to fix a bug in pazrameter order in the multiple inductioncoq
2006-02-23Ajout 'exists! x:A, P (suite)herbelin
2006-02-23Ajout 'exists! x:A, Pherbelin
2006-02-22majcoq
2006-02-22Minimum pour documentation TeX de la biblioherbelin
2006-02-22Work on recursive definitionscoq
2006-02-22Add vernacular file for subtaccoq
2006-02-22MAJherbelin
2006-02-22Julien:bertot
2006-02-21majcoq
2006-02-21Work with binder lists, problem of tyconscoq
2006-02-21Latest fixes, should work fine now for non recursive definitions, although st...coq
2006-02-20majcoq
2006-02-20Fix minor bugcoq
2006-02-20Forgot a filecoq
2006-02-20Monday work, working with coercions and implicit argscoq
2006-02-20Forgot another file...coq
2006-02-20Forgot one filecoq
2006-02-20Change in subtac modulescoq
2006-02-20Rewrite of the subtac tactic, needs some work on implicit arguments.coq