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