index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
inductiveops.mli
Commit message (
Expand
)
Author
Age
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
Fonctions retournant les arits des constructeurs et inductifs
herbelin
2006-01-30
*
Moving subst_inductive from tacinterp to inductiveops for better for reuse in...
herbelin
2005-02-18
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2005-01-14
*
Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...
herbelin
2004-08-24
*
Nouvelle en-tête
herbelin
2004-07-16
*
Ajout mis_constructor_nargs_env
herbelin
2003-11-18
*
correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...
letouzey
2002-12-13
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Ajout map_inductive_type et map_ind_family
herbelin
2002-06-13
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
Ajout make_arity_signature
herbelin
2001-11-20
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05