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
*
Ajout lemmes arithmetiques
mohring
2001-04-08
*
ajout des lemmes Zimmerman
mohring
2001-04-08
*
Ajout de lemmes sur les booleens
mohring
2001-03-30
*
Introduction d'une preuve de False_rec
mohring
2001-03-30
*
Bibliotheque Num
mohring
2001-03-26
*
entetes
filliatr
2001-03-15
*
Renommage des variables dans les schémas d'induction
herbelin
2001-02-14
*
modif de la syntax: assoc a droite pour Ring
mayero
2001-02-08
*
simplification du make depend; fonctions de stat. util. memoire dans certains...
filliatr
2001-02-08
*
*** empty log message ***
mohring
2001-02-01
*
- coqc : option -image
filliatr
2001-02-01
*
Modif de l'axiomatisation pour enlever les /\ de _ne
mayero
2001-01-25
*
Ajout d'un parseur d'entiers sous forme de pattern
herbelin
2001-01-19
*
Essai d'axiomatisation des numeral
mohring
2001-01-15
*
Ajout de commentaire coqweb
mohring
2001-01-15
*
corr bug -
mayero
2001-01-11
*
Mise a jour Rbase
mohring
2001-01-11
*
Meta Definition -> Tactic Definition
delahaye
2001-01-09
*
Tactic Definition -> Meta Definition
delahaye
2001-01-09
*
Ajout du Let pour le langage de tactiques
delahaye
2000-12-29
*
*** empty log message ***
mayero
2000-12-22
*
Bug d'affichage à cause des << ... >>
herbelin
2000-12-21
*
Oublié de supprimer du code mort
herbelin
2000-12-20
*
Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...
herbelin
2000-12-20
*
Renommages autour de NewInduction
herbelin
2000-12-18
*
pb niveau
mayero
2000-12-15
*
Prise en compte `?' dans les `` ``
herbelin
2000-12-06
*
Reparation d'un bug de pretty-print
delahaye
2000-12-05
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
Elimination du '
delahaye
2000-11-28
*
Remettre une section dans fast_integer pour contourner un bug de définition ...
herbelin
2000-11-27
*
La bonne modif des Unfold
herbelin
2000-11-27
*
Suppression de Unfold inutile et maintenant échouant
herbelin
2000-11-27
*
Changement du parseur par défaut dans Syntax
herbelin
2000-11-27
*
Le nouvel Induction s'appelle NewInduction
herbelin
2000-11-26
*
Petite simplif due au nouveau Tauto
delahaye
2000-11-24
*
Ajout d'une syntaxe pour Reals.
mayero
2000-11-23
*
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
[next]