aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/evar_tactics.ml
Commit message (Expand)AuthorAge
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* 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
* Instantiation of evars after instantiate (closes #1672).Gravatar glondu2008-02-04
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
* Suppression de code mortGravatar notin2007-02-01
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* Changement des named_contextGravatar gregoire2005-12-02
* hiding the meta_map in evar_defsGravatar barras2004-09-15
* evar tactic bugfixGravatar corbinea2004-09-14
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
* unification encore...Gravatar barras2004-09-08
* Protection contre un indice d'evar égal à 0Gravatar herbelin2004-08-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
* more evar stuffGravatar corbinea2004-06-28