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
*
Allègement de l'affichage des références par le printer si possible
herbelin
2007-01-22
*
Ajout d'une option de débogage pour expliciter l'instance des evars
herbelin
2007-01-11
*
Variable print_instances pour déboguer les instances d'evar
herbelin
2006-12-12
*
Notations:
herbelin
2006-10-09
*
Annulation de l'essai de changement de sémantique du %scope (révision 9208).
herbelin
2006-10-06
*
Essai de changement de sémantique du %scope :
herbelin
2006-10-05
*
Extension des motifs disjonctifs au cas de disjonction de motifs multiples
herbelin
2006-07-03
*
Added {measure x f} as a valid recursion order.
msozeau
2006-06-22
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
- Distinction explicite des parties paramètres et arguments dans le type
herbelin
2006-04-27
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
- 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
[next]