index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
constrextern.ml
Commit message (
Expand
)
Author
Age
*
- Utilisation d'abbréviations pour les types intervenant dans RCases
herbelin
2006-04-26
*
Timide tentative de clarification du statut de l'opérateur de filtrage
herbelin
2006-04-24
*
Amendement impression evar pour affichage des Meta par 'info'
herbelin
2006-03-31
*
- Correction bug calcul mind_consnrealargs, introduit à la révision
herbelin
2006-03-22
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
Version préliminaire d'inversion de la compilation du filtrage
herbelin
2006-01-16
*
Résidus du traducteur v7 -> v8
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Prise en compte de notations numérales définies au niveau utilisateur + tra...
herbelin
2006-01-08
*
Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ...
herbelin
2006-01-05
*
Suppression des coercions non seulement avant l'affichage des notations mais ...
herbelin
2006-01-04
*
Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...
herbelin
2005-12-30
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)
herbelin
2005-11-21
*
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
*
Bug affichage rawconstr
herbelin
2005-02-07
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-24
*
Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...
herbelin
2004-12-22
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
Nouvelle en-tête
herbelin
2004-07-16
*
Amélioration affichage coercions vers Funclass
herbelin
2004-06-02
*
Heuristique pour traduire if-then-else quand le re-typage echoue
herbelin
2004-03-30
*
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2004-03-28
*
correction bug de facto des fix (2e)
barras
2004-03-14
*
correction bug de facto des fix
barras
2004-03-14
*
correction bug de choix de noms courts avec Suresnes/BDD
barras
2004-03-14
*
correction de bugs des points fixes
barras
2004-03-08
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Keep structure information for Fixpoint declaration and Fix terms
bertot
2004-02-26
*
- fixed the Assert_failure error in kernel/modops
barras
2004-02-18
*
Bug coercions imbriquees + suppression des coercions avant filtrage sur notat...
herbelin
2004-02-18
*
Correction bug affichage en presence de '{ _ }'
herbelin
2004-02-12
*
Décomposition automatique des règles d'analyse syntaxique pour les
herbelin
2004-02-12
*
Relachement condition pour afficher @ en cas d'explicitation d'implicites
herbelin
2004-02-03
*
Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...
herbelin
2004-01-29
*
Bug activation erronée du traducteur en v8
herbelin
2004-01-27
*
reparation de qqs bugs du traducteur
barras
2004-01-26
*
Traduction PolyList/List dans la qualification
herbelin
2003-12-21
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
'Eval' protege dans Ppconstrnew; eval n'a pas le meme besoin
herbelin
2003-12-15
*
Renommages discrets dans RIneq et Znumtheory
herbelin
2003-11-29
*
Suite commit precedent
herbelin
2003-11-27
*
Qualification des noms utilisateurs en cas de collision avec un nom nouveau
herbelin
2003-11-27
*
Traduction de @; simplification traduction des ident
herbelin
2003-11-26
*
modif lexer: ident peut commencer par _
barras
2003-11-25
*
ajout Pnat et Pcompare_antisym
herbelin
2003-11-21
[next]