aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/decl_proof_instr.ml
Commit message (Expand)AuthorAge
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* fixed czar bug with parametric inductivesGravatar corbinea2009-10-27
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* pushed evar reduction in kernelGravatar barras2009-02-06
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* About "apply in":Gravatar herbelin2008-12-09
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* 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-12-20 05:41:08 +0000