aboutsummaryrefslogtreecommitdiff
path: root/tactics/evar_tactics.ml
AgeCommit message (Expand)Author
2012-11-25Monomorphization (tactics)ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-02Noise for nothingpboutill
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2010-09-17Fixed a problem introduced in r12607 after pattern_of_constr servedherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
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-04-20 12:56:26 +0000