index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
*
*** empty log message ***
barras
2003-03-21
*
reparations suite a la nouvelle syntaxe:
barras
2003-03-14
*
Ajout réaffichage SubClass
herbelin
2003-03-13
*
*** empty log message ***
barras
2003-03-12
*
Renommage indpar pour usage plus general
herbelin
2003-03-12
*
Bug délimiteur de scope en vieil affichage ast
herbelin
2003-03-04
*
Retour vieil afficheur
herbelin
2003-03-03
*
Interpretation des entiers dans les reels via les scopes
desmettr
2003-02-27
*
Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'...
herbelin
2003-02-27
*
Correction test token normal
herbelin
2003-02-27
*
Le lexeur et Notation savent reconnaître si un unicode des blocs
herbelin
2003-02-27
*
Retour nouvel afficheur
herbelin
2003-02-27
*
Affinement entree annot
herbelin
2003-02-17
*
Debugger plus informatif
delahaye
2003-02-13
*
Ajout du traducteur
desmettr
2003-02-05
*
Pour satisfaire ProofGeneral
coq
2003-01-31
*
Adds a possibility to construct a term as if it had been parsed through
bertot
2003-01-30
*
Deux p\'tits trucs ;)
coq
2003-01-27
*
I changed the interface to make sure SearchAbout is defined according to
bertot
2003-01-22
*
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2003-01-19
*
Rétablissement pr_pattern
herbelin
2003-01-19
*
Bugs affichage
herbelin
2003-01-16
*
Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...
herbelin
2003-01-15
*
Nouvelle interprétation des nombres réels
desmettr
2003-01-15
*
Export M + Module M <: SIG
coq
2003-01-09
*
Retour printer ast pour V7.4
herbelin
2003-01-07
*
SearchAbout
filliatr
2003-01-06
*
Prise en compte notations dans les extensions de motiff
herbelin
2002-12-28
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Affinement affichage
herbelin
2002-12-21
*
Plus de notation cablees dans 'annot'
herbelin
2002-12-21
*
Petit netoyage dans lib
coq
2002-12-19
*
bug: Global.env() executé au chargement -> eta-expansion
letouzey
2002-12-19
*
Meilleure factorisation des entrées NEXT internes
herbelin
2002-12-15
*
Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxe
herbelin
2002-12-15
*
Pas de 0 dans positive
herbelin
2002-12-15
*
possibilité de faire Print M avec M module ou modtype au lieu de Print Modul...
letouzey
2002-12-13
*
Ajout du vernac Proof with
gregoire
2002-12-12
*
Bugs divers
herbelin
2002-12-10
*
Ajout options -v7 et -v8, et commandes V7only et V8only
herbelin
2002-12-10
*
Problèmes et améliorations affichage; Changement Simpl
herbelin
2002-12-09
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...
herbelin
2002-12-04
*
Modification Require From
mohring
2002-12-04
*
la table PARAMETER n'existe plus (mergé dans la table CONSTANT)
letouzey
2002-12-03
*
bug de non-indépendance des règles d'affichage et parsing vis à vis du nom...
herbelin
2002-12-03
*
bugs d'affichage (confusion key/scope dans les délimiteurs)
herbelin
2002-12-03
*
Calcul de l'associativité même pour les Grammar avec plusieurs clauses
herbelin
2002-12-03
*
Le '.' peut faire partie d'un token
herbelin
2002-12-03
*
Remplacement de Syntactic Definition par Notation
herbelin
2002-12-02
[next]