aboutsummaryrefslogtreecommitdiff
path: root/tactics/decl_proof_instr.ml
AgeCommit message (Expand)Author
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-07-24Declarative language: fixed the generation of fixpoints for induction proofs.corbinea
2007-07-06extension of the rename tactic: the following is now allowed: letouzey
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
2007-04-27fixed glitch in escapecorbinea
2007-04-26fin des conclusions multiplescorbinea
2007-04-18debug plus poussé induction dépendantecorbinea
2007-04-16fix bug with dependent inductive familiescorbinea
2007-02-09bugfix sufficescorbinea
2007-01-31redirection of errors in coqide + dynamic warning printer (needed for tm_egg)corbinea
2007-01-29finalized sufficescorbinea
2007-01-28"suffices" implemented + syntax cleanupcorbinea
2007-01-25decl mode: anonymous factscorbinea
2007-01-22Correction du bug #1315:notin
2007-01-22changes in declarative language : by term using tacticcorbinea
2006-11-19Raffinement de l'unification de "apply": mémorisation de certainsherbelin
2006-09-26fixed error mesg in decl modecorbinea
2006-09-20Declarative Proof Language: main commitcorbinea
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 12:24:30 +0000