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
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...
herbelin
2005-12-17
*
Changement des named_context
gregoire
2005-12-02
*
parametres inductifs
mohring
2005-11-28
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Types inductifs parametriques
mohring
2005-11-02
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Expansion du prédicat du 'match' vis à vis de la dépendance en le terme fi...
herbelin
2004-08-24
*
Nouvelle en-tête
herbelin
2004-07-16
*
Eta-expansion du predicat dans build_indrec (suite)
herbelin
2004-07-11
*
Eta-expansion du predicat pas seulement pour make_case mais aussi pour build_...
herbelin
2004-07-11
*
Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...
herbelin
2003-09-12
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
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