aboutsummaryrefslogtreecommitdiff
path: root/tactics/evar_tactics.ml
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2008-09-12Add a type argument to letin_tac instead of using casts and recomputingmsozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-02-04Instantiation of evars after instantiate (closes #1672).glondu
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-02-01Suppression de code mortnotin
2006-09-20Declarative Proof Language: main commitcorbinea
2006-04-28Standardisation du nom des méthodes de Evdherbelin
2006-01-16- Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesherbelin
2005-12-02Changement des named_contextgregoire
2004-09-15hiding the meta_map in evar_defsbarras
2004-09-14evar tactic bugfixcorbinea
2004-09-12inclusion de meta_map dans evar_defsbarras
2004-09-08unification encore...barras
2004-08-03Protection contre un indice d'evar égal à 0herbelin
2004-07-16Nouvelle en-têteherbelin
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-28more evar stuffcorbinea
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:56:46 +0000