index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
impargs.mli
Commit message (
Expand
)
Author
Age
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Moving centralised discharge into dispatched discharge_function; required to ...
herbelin
2005-02-18
*
Nouvelle en-tête
herbelin
2004-07-16
*
Utilisation de noms dans 'Implicit Arguments [...]'
herbelin
2003-09-23
*
Mise en place d'implicites par noms en v8
herbelin
2003-09-21
*
Affichage forcé des implicites contextuels si pas de contexte connu
herbelin
2003-04-10
*
Synchronisation séparée des implicites pour l'affichage du traducteur;
herbelin
2003-04-09
*
Correction Show Implicits
herbelin
2003-04-09
*
Réorganisation de Impargs + mise en place d'une infrastructure
herbelin
2003-04-09
*
Ajout des options "Set Contextual Implicits" et "Set Strict Implicits
herbelin
2002-12-02
*
Des critères plus fins d'analyse des implicites automatiques; meilleur affic...
herbelin
2002-10-28
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
GROS COMMIT:
barras
2001-11-05
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
entetes
filliatr
2001-03-15
*
Ré-introduction des implicites à la volée dans la définition des inductifs
herbelin
2001-01-27
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
implicites manuels
filliatr
2000-11-21
*
separation calcul des implicites et declaration des constantes / inductifs / ...
filliatr
2000-11-21
*
Ajout implicits_of_global + accès par noms longs
herbelin
2000-11-20
*
L'état implicite des définitions survivant au discharge redevient celui du ...
herbelin
2000-10-23
*
suppression de Fw pour les implicites
herbelin
2000-05-03
*
modifs pour premiere edition de liens
filliatr
1999-12-02
*
Intégration du Termast et du Retyping de HH, et modifications connexes
herbelin
1999-12-01
*
poursuite de Vernacentries
filliatr
1999-12-01
*
module Termast
filliatr
1999-11-26
*
- un effort sur la doc (ocamlweb)
filliatr
1999-09-19