aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/evar_tactics.ml
Commit message (Expand)AuthorAge
* Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envGravatar herbelin2013-01-29
* Monomorphization (tactics)Gravatar ppedrot2012-11-25
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* 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