aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/decl_proof_instr.ml
Commit message (Expand)AuthorAge
* Add more information to IllFormedRecBody exceptions, to show the exactGravatar msozeau2008-02-08
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Declarative language: fixed the generation of fixpoints for induction proofs.Gravatar corbinea2007-07-24
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Contrôle de la compatibilité de apply via une information dans lesGravatar herbelin2007-05-28
* fixed glitch in escapeGravatar corbinea2007-04-27
* fin des conclusions multiplesGravatar corbinea2007-04-26
* debug plus poussé induction dépendanteGravatar corbinea2007-04-18
* fix bug with dependent inductive familiesGravatar corbinea2007-04-16
* bugfix sufficesGravatar corbinea2007-02-09
* redirection of errors in coqide + dynamic warning printer (needed for tm_egg)Gravatar corbinea2007-01-31
* finalized sufficesGravatar corbinea2007-01-29
* "suffices" implemented + syntax cleanupGravatar corbinea2007-01-28
* decl mode: anonymous factsGravatar corbinea2007-01-25
* Correction du bug #1315:Gravatar notin2007-01-22
* changes in declarative language : by term using tacticGravatar corbinea2007-01-22
* Raffinement de l'unification de "apply": mémorisation de certainsGravatar herbelin2006-11-19
* fixed error mesg in decl modeGravatar corbinea2006-09-26
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:03:41 +0000