index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
Nettoyage
herbelin
2000-11-21
*
ajout de theories/Wellfounded
filliatr
2000-11-21
*
separation calcul des implicites et declaration des constantes / inductifs / ...
filliatr
2000-11-21
*
Bug dans la règle de syntaxe de ex2
herbelin
2000-11-20
*
Nettoyage + prise en compte noms longs
herbelin
2000-11-20
*
Suppression de la section fast_integer qui cachait le nom du module éponyme
herbelin
2000-11-20
*
Retour a la version 1.1
herbelin
2000-11-13
*
Y avait des '.' non suivis d'un séparateur
herbelin
2000-11-11
*
mise-a-jour, ajouts de quelques truc...
mayero
2000-11-10
*
Finalement PolyListSyntax est necessaire (la redondance venait d'une confusio...
herbelin
2000-11-10
*
Modification de la table des tactic Definitions pour eviter l'ecriture
mohring
2000-11-07
*
Changement/extension dans les noms de parseurs de Grammar
herbelin
2000-11-07
*
Orthographe
herbelin
2000-11-07
*
Plus besoin de débrancher la preuve qui ne passait pas
herbelin
2000-11-05
*
Plus besoin de rajouter "Require Plus"
herbelin
2000-11-05
*
Pour ne plus éviter temporairement le "Auto with zarith" !
herbelin
2000-11-05
*
Suppression d'Intuition (trop intelligent?)
delahaye
2000-10-30
*
Pour eviter temporairement le "Auto with zarith"
delahaye
2000-10-30
*
Passage command -> constr
herbelin
2000-10-27
*
g_natsyntax et g_zsyntax maintenant toujours linkes
filliatr
2000-10-27
*
Mise a jour TheoryList
mohring
2000-10-27
*
Retire les parentheses autour des tactiques
mohring
2000-10-26
*
Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...
herbelin
2000-10-18
*
Parentheses
herbelin
2000-10-12
*
Finalement, encore un Simpl inutile
herbelin
2000-10-10
*
Parenthèses pour les tactiques
herbelin
2000-10-06
*
Changement dans la stratégie de réduction du Fix par Simpl
herbelin
2000-10-06
*
Un usage en moins de l'axiome eq_rec_eq
herbelin
2000-10-06
*
Remplacement de la tactique Program (partiel)
herbelin
2000-10-05
*
Commit malencontreux sur précédente version
herbelin
2000-10-04
*
Mise en conformité nouveau Simpl pour Fix
herbelin
2000-10-04
*
Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...
herbelin
2000-07-28
*
portage Refine
filliatr
2000-07-20
*
correction
mayero
2000-07-04
*
ajouts
mayero
2000-07-03
*
Traduction de syntaxe vers ltac
delahaye
2000-07-03
*
Séparation des caractères spéciaux par un blanc
herbelin
2000-07-01
*
Retrait des parenthèses inutiles autour des tactiques
herbelin
2000-07-01
*
Require Plus ajoute
filliatr
2000-06-21
*
theories/Reals
filliatr
2000-06-21
*
theories/Relations
filliatr
2000-06-21
*
theories/Sets
filliatr
2000-06-21
*
theories/Lists
filliatr
2000-06-21
*
Séparation des tokens -> et ~
herbelin
2000-05-22
*
Changement nommage des hypothèses; parenthèses pour les tactiques
herbelin
2000-05-22
*
Parenthèses
herbelin
2000-05-22
*
parethèses de tactiques
herbelin
2000-05-18
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
portage Omega (mais toujours pas Zpower et Zlogarithm)
filliatr
2000-05-02
*
Bug affichage Error et Value
herbelin
2000-04-30
[next]