index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
field
Commit message (
Expand
)
Author
Age
*
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...
herbelin
2003-11-29
*
petits changements de syntaxe
barras
2003-11-12
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Cacher les .v8
herbelin
2003-10-03
*
Ajout fonctions syntaxe v8 pour contrib MapleMode
herbelin
2003-09-23
*
Système de renommage des noms de tactiques Ltac
herbelin
2003-09-22
*
Passage à la V8 par défaut
herbelin
2003-09-22
*
Pour accomoder autant le printer v8 que v7
herbelin
2003-09-06
*
Protection contre les types sans corps associé
herbelin
2003-09-06
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Explicitation arguments de eq
herbelin
2003-04-11
*
Mauvaise resolution conflit dans commit precedent
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Légères simplifications code de Field; message d'erreur si pas égalité
herbelin
2003-04-03
*
remplace == par = dans la tactique field pour que le debugger marche a nouvea...
narboux
2003-04-01
*
Fail 1 pour traverser le match
herbelin
2003-04-01
*
Plus de eqT; message Fail
herbelin
2003-03-31
*
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2003-03-31
*
*** empty log message ***
barras
2003-03-12
*
Utilisation de 'Recursive' pour les tactiques récursives
herbelin
2003-01-20
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
MAJ syntaxe
herbelin
2002-11-14
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Protection des tactiques contre l'utilisation sans le bon contexte de thories
herbelin
2002-06-03
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
Fix d'un bug sur le test des inverses
delahaye
2002-03-19
*
Meilleure gestion de la reduction dans Field
delahaye
2002-03-17
*
Oubli d'un quote
herbelin
2001-12-18
*
oubli: changement de nil en nilT
mayero
2001-11-14
*
Changement de list en listT, cons en consT et app en appT
mayero
2001-11-14
*
GROS COMMIT:
barras
2001-11-05
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Correction due au changement de semantique de Match
delahaye
2001-09-21
*
Transparent
barras
2001-09-20
*
Parsing
herbelin
2001-08-10
*
Ajout d'un Ring pour setoides
clrenard
2001-07-10
*
Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...
herbelin
2001-07-02
*
Reduction du terme preuve fourni par Field
delahaye
2001-06-27
*
Reduction tres significative du terme preuve
delahaye
2001-06-27
*
Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...
herbelin
2001-06-25
*
Changement de la structure des points fixes
barras
2001-05-03
*
Suppression d'une partie de code commente
delahaye
2001-04-24
*
Ajout des entetes
delahaye
2001-04-20
*
Ajout de Field
delahaye
2001-04-19