index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
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
*
export de la fonction Reductionops.find_conclusion pour l'extraction
letouzey
2002-04-08
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
petite erreur dans le typage des let-in
barras
2002-03-28
*
Prise en compte des dependances dans la tactique Case
mohring
2002-03-26
*
Décomposition de l'application n-aire en application binaire pour que Patter...
herbelin
2002-03-21
*
Nouveau Rewrite-in plus economique
barras
2002-03-04
*
Nouveau comportement: Delta ne s'applique pas aux variables liées par un let
herbelin
2002-03-01
*
typage du produit: type_judgment appele avec contexte incorrect
barras
2002-02-19
*
meilleur message d'erreur lorsqu'on type une evar qui n'existe pas
barras
2002-02-19
*
Le type des evars transformees en meta n'etait pas normalise, et des Evars
barras
2002-02-19
*
bug #134: on appelait solve_simple_eqn avec une evar qui etait resolue
barras
2002-02-18
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
petite modif pour ne pas expanser trop de let pendant l'unification
barras
2002-02-12
*
substitution et pattern modulo let
barras
2002-02-11
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
exceptionmal ratrappee
barras
2002-02-04
*
changement generation de schema d'elimination, False_rec est primitif, Constr...
mohring
2002-01-31
*
Correction bug 'Check [b]if b then O else O'
herbelin
2002-01-25
*
code mort
herbelin
2002-01-24
*
Réparation bug 'known_dependent'
herbelin
2002-01-24
*
warning en mode verbeux seulement
filliatr
2002-01-21
*
Le chargement des coercions est nécessaire même si le module n'est pas ouvert
herbelin
2002-01-18
*
Amélioration affichage échec lookup_eliminator
herbelin
2002-01-17
*
Correction d'un problème avec les motifs anonymes dépendant dans des argume...
herbelin
2002-01-16
*
Correction de de Bruijn incorrect pour le cas de dépendances vers l'avant
herbelin
2002-01-15
*
Non dépliage des Fix non réductibles dans Hnf
herbelin
2001-12-20
*
Insertion unification non seulement en tête mais à l'intérieur des motifs ...
herbelin
2001-12-19
*
Grossière erreur de typage
herbelin
2001-12-18
*
Nettoyage exceptions liées au vieux Case
herbelin
2001-12-18
*
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
*
compat ocaml 3.03
filliatr
2001-12-13
*
Mise en place de coercion dans les motifs
herbelin
2001-12-11
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
La mise en forme normale du prédicat d'élimination était un peu trop viole...
herbelin
2001-11-22
*
Quelques autres petits problèmes résolus...
herbelin
2001-11-21
*
Simplification de la propagation du prédicat, bugs, et messages d'erreurs
herbelin
2001-11-21
*
Solution partielle au problème des alias dépendants pour les rendre compati...
herbelin
2001-11-21
*
Prise en compte des coercions pour typer les branches lorsqu'il y a une contr...
herbelin
2001-11-21
*
Ajout make_arity_signature
herbelin
2001-11-20
*
Correction bug contrainte de valeur trop restrictive sur le typage du type du...
herbelin
2001-11-20
*
Bug mauvaise instance
herbelin
2001-11-20
*
Fusion de declare/add_constant, declare/add_parameter et add_discharged_constant
herbelin
2001-11-20
*
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
*
Remise en place du Cast pour Correctness
herbelin
2001-11-19
[next]