index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
eauto.ml4
Commit message (
Expand
)
Author
Age
*
Slight cleanup of refl_omega.ml : in particular it uses now list
letouzey
2007-07-11
*
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-22
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
Suite unification apply et eapply (l'un et l'autre profite maintenant
herbelin
2007-04-16
*
Essai de partage de code entre apply et eapply
herbelin
2007-04-15
*
Correction d'une tentative incorrecte (révision 9266) de clarification
herbelin
2006-10-25
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Debugging en syntaxe v8
herbelin
2006-02-05
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2006-01-24
*
Export eassumption
herbelin
2006-01-19
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...
herbelin
2005-12-21
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
* added subst_evaluable_reference
sacerdot
2004-12-07
*
unification encore...
barras
2004-09-08
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
New tactics : econstructor, eleft, eright, esplit
clrenard
2003-11-17
*
Nettoyage
herbelin
2003-11-08
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
*** empty log message ***
barras
2003-03-12
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Option pour rendre les vérifications du refiner optionnelle
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...
herbelin
2002-06-05
*
Fichiers tactics/*.ml4 remplacent les tactics/*.v
herbelin
2002-05-29