index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
detyping.ml
Commit message (
Expand
)
Author
Age
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
Nouvelle en-tête
herbelin
2004-07-16
*
Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ...
herbelin
2004-07-11
*
Double bug d'affichage des cases dépendants (bug #784)
herbelin
2004-06-28
*
Correction affichage v8 des records avec let (bug #798)
herbelin
2004-06-27
*
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2004-03-28
*
bug de PP des fix (coqbugs #574)
barras
2004-03-24
*
bug affichage des cofix
barras
2004-03-09
*
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
*
Inclusion des annotations de type des filtrages dans 'Set Printing All'
herbelin
2004-02-26
*
Relachement condition pour declarer un inductif dans la table des 'If'; contr...
herbelin
2004-02-03
*
Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...
herbelin
2004-01-29
*
Substitution dans REvar; reparation bug 277
herbelin
2003-12-19
*
Changement de l'afficheur pour que les variables liées aient un nom indépen...
herbelin
2003-09-23
*
open superflu
herbelin
2003-09-12
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
Bug détypage du fix
herbelin
2003-08-12
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Factorisation de detype_case pour utilisation par l'afficheur de pattern
herbelin
2003-06-10
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...
herbelin
2003-04-27
*
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin
2003-03-29
*
*** empty log message ***
barras
2003-03-12
*
Bug affichage let destructurant
herbelin
2003-02-02
*
Problème de désynchronisation des variables du type et du corps d'un point-...
herbelin
2003-01-15
*
Affinement affichage
herbelin
2002-12-21
*
apres correction du probleme de Global.env, retour du mis_constr_nargs_env
letouzey
2002-12-19
*
ma bidouille marche pas...
letouzey
2002-12-17
*
correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...
letouzey
2002-12-13
*
Problèmes et améliorations divers affichage
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
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
*
Utilisation d'une construction spéciale SECVAR pour gérer la
herbelin
2002-05-14
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
substitution et pattern modulo let
barras
2002-02-11
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
compat ocaml 3.03
filliatr
2001-12-13
*
Bug nommage des fonctions définies par récursion mutuelle
herbelin
2001-11-19
*
Re-installation de l'affichage des globaux par des noms courts
herbelin
2001-11-19
*
GROS COMMIT:
barras
2001-11-05
*
Reorganisation de Goption. Passage des options l'utilisant en synchrone
letouzey
2001-10-30
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Bug d'affichage du prédicat, bug d'affichage des clauses en présence de dé...
herbelin
2001-10-03
*
Réparation des options Set Printing and co
herbelin
2001-09-21
*
erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies
barras
2001-09-04
*
Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...
herbelin
2001-07-21
[next]