index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
evar_tactics.ml
Commit message (
Expand
)
Author
Age
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fixing bug #2308 ("instantiate" tactic did not comply with
herbelin
2009-04-24
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
Add a type argument to letin_tac instead of using casts and recomputing
msozeau
2008-09-12
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Instantiation of evars after instantiate (closes #1672).
glondu
2008-02-04
*
Correction d'un bug dans l'affichage du message d'erreur real_clean
herbelin
2007-05-29
*
Suppression de code mort
notin
2007-02-01
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
Changement des named_context
gregoire
2005-12-02
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
evar tactic bugfix
corbinea
2004-09-14
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
unification encore...
barras
2004-09-08
*
Protection contre un indice d'evar égal à 0
herbelin
2004-08-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
more evar stuff
corbinea
2004-06-28