index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
pretyping.ml
Commit message (
Expand
)
Author
Age
*
Backtrack sur la substitution combinée avec l'instanciation en réponse à l...
herbelin
2005-03-15
*
A défaut de substitution paresseuse ou explicite, ajout d'une substitution o...
herbelin
2005-03-10
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
Correction de la précédence des contexts de variables rel, ltac et var
herbelin
2005-02-02
*
Relâchement obligation d'une contrainte de type sur les Hole en position ter...
herbelin
2004-12-06
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...
herbelin
2004-08-24
*
Nouvelle en-tête
herbelin
2004-07-16
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
Prise en compte d'un type dont la sorte est une evar
herbelin
2004-04-29
*
Correction incapacité à gérer les annotations de type dépendantes pour le...
herbelin
2004-04-27
*
Typo
herbelin
2004-03-29
*
Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...
herbelin
2004-03-28
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...
herbelin
2004-02-04
*
Backtrack sur recuperation de noms a partir du type, car casse la correction ...
herbelin
2004-02-03
*
Reparation d'une rupture (en presence de types implicites) de l'invariant que...
herbelin
2004-01-29
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
Deplacement subst_rawconstr dans Rawterm
herbelin
2003-11-19
*
Amelioration message d'erreur pour ltac
herbelin
2003-11-04
*
Oubli du type du terme a filtrer quand pas d'argument dans la traduction de case
herbelin
2003-09-29
*
Changement de l'afficheur pour que les variables liées aient un nom indépen...
herbelin
2003-09-23
*
Bug predicat old Case
herbelin
2003-09-10
*
Bug predicat let-tuple
herbelin
2003-09-09
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Bug et améliorations diverses
herbelin
2003-08-12
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Rien d'important
herbelin
2003-05-13
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Amélioration messages d'erreur non inférence implicites
herbelin
2002-09-03
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
reparation pretyping ROldCase dans le cas let
filliatr
2002-07-02
*
factorisation code dans make_dep_of_undep
filliatr
2002-07-02
*
*** empty log message ***
mohring
2002-06-26
*
*** empty log message ***
mohring
2002-06-26
*
Deuxième passe sur la localisation des messages d'erreurs sur les evars non ...
herbelin
2002-04-11
*
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2002-04-10
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
Le type des evars transformees en meta n'etait pas normalise, et des Evars
barras
2002-02-19
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
Correction bug 'Check [b]if b then O else O'
herbelin
2002-01-25
*
Nettoyage exceptions liées au vieux Case; réparation du try with UserError ...
herbelin
2001-12-18
*
Contournement du problème des evars de type, typées par défaut dans Type (...
herbelin
2001-12-13
*
Contournement du problème des evars de type, typées par défaut dans Type
herbelin
2001-12-13
[next]