index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
indrec.ml
Commit message (
Expand
)
Author
Age
...
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
*** empty log message ***
barras
2003-03-12
*
Bug en présence de let-in
herbelin
2003-01-15
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Un peu (plus) d'ordre dans Nametab...
coq
2002-09-24
*
Renoncement à distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
changement generation de schema d'elimination, False_rec est primitif, Constr...
mohring
2002-01-31
*
code mort
herbelin
2002-01-24
*
warning en mode verbeux seulement
filliatr
2002-01-21
*
Amélioration affichage échec lookup_eliminator
herbelin
2002-01-17
*
compat ocaml 3.03
filliatr
2001-12-13
*
GROS COMMIT:
barras
2001-11-05
[prev]