index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
ring
/
quote.ml
Age
Commit message (
Expand
)
Author
2002-03-04
Nouveau Rewrite-in plus economique
barras
2001-11-05
GROS COMMIT:
barras
2001-10-09
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-08-10
Parsing
herbelin
2001-05-03
Changement de la structure des points fixes
barras
2001-04-09
réparation Quote
filliatr
2001-04-06
correction d'un bug de Quote
filliatr
2001-03-15
entetes
filliatr
2001-03-01
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-02-16
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-14
Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...
herbelin
2001-01-12
Now Ring does not perform any more the same reduction twice.
sacerdot
2000-11-29
Nouveau long long avec Coq en tête
herbelin
2000-11-28
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-26
Appel des constantes globaux par des noms absolus
herbelin
2000-11-23
Simplification de l'accès aux globaux
herbelin
2000-11-22
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-20
Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...
herbelin
2000-10-01
Renommage AppL en App
herbelin
2000-09-14
Abstraction de constr
herbelin
2000-09-12
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-10
Ajout d'un LetIn primitif.
herbelin
2000-07-21
*) -> i*)
filliatr
2000-06-21
Ring
filliatr