index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tauto.ml4
Commit message (
Expand
)
Author
Age
...
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
More compatibility fixes, revert the tauto fix that prevented
msozeau
2008-07-25
*
Tauto breaking not only binary "conjunctions" seems like a bad idea
msozeau
2008-07-24
*
A try at allowing matching on applications as a binary syntax node by default.
msozeau
2008-07-22
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Modifications diverses et variées :
herbelin
2008-03-30
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Nouvelle en-tête
herbelin
2004-07-16
*
*** empty log message ***
barras
2003-12-23
*
petits changements de syntaxe
barras
2003-11-12
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
Passage à la V8 par défaut
herbelin
2003-09-22
*
switching back to old tauto
corbinea
2003-07-03
*
added hints into Ground
corbinea
2003-07-02
*
*** empty log message ***
courant
2003-06-27
*
Preservation affichage des ?n en V7
herbelin
2003-05-22
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
Fixed Relative names not,iff in Camlp4 quotation.
corbinea
2003-03-28
*
Introducing Christine's Intuition1 and adding some invertible hyps.
corbinea
2003-03-18
*
Changed Tauto so it displays less 'Unfold not iff'
corbinea
2003-02-26
*
Suppression de l'élimination des existentiels dans LinearIntuition.
corbinea
2003-02-05
*
Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).
corbinea
2003-01-23
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
correction bugs Tauto
courant
2002-07-19
*
Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3|- ?]
corbinea
2002-07-17
*
Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait
courant
2002-07-15
*
Nettoyage
herbelin
2002-05-30
*
Fichiers tactics/*.ml4 remplacent les tactics/*.v
herbelin
2002-05-29
*
Correction of a bug in Intuition (no more decomposition of dependent pairs).
corbinea
2002-05-22
*
Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
herbelin
2002-05-15
*
Finalement VTactic est gardé pour y plonger les tactiques ML, le
herbelin
2002-05-15
*
- Changement de l'ordre de filtrage dans "Match Context"
herbelin
2002-05-14
*
nettoyage code
courant
2002-05-02
*
*** empty log message ***
courant
2002-04-08
*
Intuition ne fait plus de Unfold des constantes (il faut les faire
courant
2002-03-21
*
Intuition now takes an (optional) tactic as parameter. This tactic is
courant
2002-03-20
*
Tauto est maintenant stable par "Intro" :
courant
2002-03-15
*
substitution et pattern modulo let
barras
2002-02-11
*
Mise en place de la réduction sous forme d'implications d'atomes en fn de tête
herbelin
2001-12-20
*
Utilisation de Hnf plutôt que Red
herbelin
2001-12-20
*
Puisque Orelse semble lier moins que THEN, ajout d'un reduce après le Orelse
herbelin
2001-12-19
*
Insertion de Red sur chaque atome dans Tauto et Intuition
herbelin
2001-12-19
*
Tentative d'amélioration du résultat de Intuition
herbelin
2001-12-19
*
compat ocaml 3.03
filliatr
2001-12-13
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Ajout du printer de tactiques + modif du Dynamic ocaml
delahaye
2001-09-30
[prev]
[next]