index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Fail n + appel de interp
delahaye
2000-07-21
*
Modifs d'interpretation de patterns
delahaye
2000-07-21
*
Modifs d'interpretation de patterns + exceptions dans le lexer
delahaye
2000-07-21
*
Pattern -> parsing
delahaye
2000-07-21
*
portage Refine
filliatr
2000-07-20
*
tests Refine
filliatr
2000-07-20
*
Quelques (*i*) pour ne pas casser oczmlweb
coq
2000-07-19
*
Adaptation pour Alpha.
delahaye
2000-07-05
*
Adaptation pour alpha.
delahaye
2000-07-05
*
correction
mayero
2000-07-04
*
ajouts
mayero
2000-07-03
*
Opaque pas encore implementee; syntax langage tactiques
filliatr
2000-07-03
*
Traduction de syntaxe vers ltac
delahaye
2000-07-03
*
Correction de Cofix
delahaye
2000-07-03
*
Plus de env et sigma dans get_arity, plus de sigma dans make_arity
herbelin
2000-07-01
*
Précalcul de la forme canonique des constructeurs et arités pour traiter le...
herbelin
2000-07-01
*
Ajout fonctions sur les arités
herbelin
2000-07-01
*
Plus de env et sigma dans get_arity, plus de sigma dans make_arity
herbelin
2000-07-01
*
Précalcul de la forme canonique des constructeurs et arités pour traiter le...
herbelin
2000-07-01
*
Séparation des caractères spéciaux par un blanc
herbelin
2000-07-01
*
Retrait des parenthèses inutiles autour des tactiques
herbelin
2000-07-01
*
Extension de find_inductive aux co-inductifs et renommage en find_rectype
herbelin
2000-07-01
*
Le bon type pour list_fold_right_and_left
herbelin
2000-07-01
*
index devenu list_index échoue maintenant avec Not_found et plus Failure
herbelin
2000-07-01
*
Bug: on tentait de déclarer un schéma d'induction pour un coinductif
herbelin
2000-07-01
*
Extension de find_inductive aux co-inductifs et renommage en find_rectype
herbelin
2000-07-01
*
fonction list_fold_left_right pas definie
filliatr
2000-06-30
*
Capture erreur de create_process
herbelin
2000-06-29
*
Ajout list_fold_right_and_left
herbelin
2000-06-29
*
MAJ
herbelin
2000-06-29
*
Utilisation du STRIP de config/Makefile pour gérer le mode profile
herbelin
2000-06-29
*
Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_of
herbelin
2000-06-29
*
Séparation des contraintes de type et de valeur dans pretyping
herbelin
2000-06-29
*
Relative prend sigma en plus pour la normalisation du message d'erreur
herbelin
2000-06-29
*
Broutilles
herbelin
2000-06-29
*
Ajout make_typed_lazy
herbelin
2000-06-29
*
Normalisation des Evar avant génération des erreurs
herbelin
2000-06-29
*
Bricoles
herbelin
2000-06-29
*
Renommage mk_unsafe_judgment en get_judgment_of
herbelin
2000-06-29
*
Extension de l'inférence des types des lambdas du prédicat
herbelin
2000-06-29
*
Achèvement abstraction du mécanisme (optionnel) de cast
herbelin
2000-06-29
*
Rien
herbelin
2000-06-29
*
Essai de simplification compte tenu de l'info de location
herbelin
2000-06-29
*
Modifs de presentation.
delahaye
2000-06-28
*
Rattrapage d'un Not_found pour les VAR's.
delahaye
2000-06-28
*
Retrait du 'strip' en cas de profiling
herbelin
2000-06-27
*
$BINDER -> BINDER
filliatr
2000-06-21
*
- $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)
filliatr
2000-06-21
*
Require Plus ajoute
filliatr
2000-06-21
*
bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...
filliatr
2000-06-21
[prev]
[next]