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
*
Évitement des noms de constructeurs dans les motifs de filtrage de "match"
herbelin
2006-12-09
*
The "clean integration of subtac" patch.
msozeau
2006-05-29
*
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
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
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
*
Standardisation du nom de subst_raw en subst_rawconstr
herbelin
2006-01-11
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Types inductifs parametriques
mohring
2005-11-02
*
Un vieux bug d'affichage des lieurs (cf bug #1005)
herbelin
2005-09-06
*
Sur le conseil de X.Leroy: x=[||] devient Array.length x=0
letouzey
2005-08-19
*
HUGE COMMIT
sacerdot
2005-01-03
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
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
[next]