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
...
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Affinement affichage
herbelin
2002-12-21
*
Petit netoyage dans lib
coq
2002-12-19
*
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
*
Commentaires
herbelin
2002-12-10
*
Essai suppression nf_betaiota dans type_of
herbelin
2002-12-09
*
Problèmes et améliorations divers affichage
herbelin
2002-12-09
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Allègement du noyau
herbelin
2002-11-18
*
Ajout de Cases dans abbreviatable constr (aconstr) [utilisé dans la
herbelin
2002-11-18
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Un revenant hors sujet
herbelin
2002-11-13
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Moins de restriction sur le commit 1.5
herbelin
2002-10-17
*
nom de fonction plus simple
barras
2002-10-15
*
Moins de restriction sur le commit précédent
herbelin
2002-10-13
*
Ajout map_rawconstr
herbelin
2002-10-13
*
Restriction sur la forme des Syntactic Definition et re-localisation en fonct...
herbelin
2002-10-12
*
retour en arriere concernant la recherche d'occurence modulo expansion des le...
barras
2002-10-09
*
Vraie substitutivite de autohints
coq
2002-10-01
*
Un peu (plus) d'ordre dans Nametab...
coq
2002-09-24
*
Amélioration messages d'erreur non inférence implicites
herbelin
2002-09-03
*
pretyping/pretyping.ml
herbelin
2002-09-03
*
correction de bugs:
barras
2002-08-16
*
Renoncement à distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
un cas inutile dans un pattern matching
letouzey
2002-07-16
*
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
*
Nouvelle version de l'algorithme de compilation du filtrage compatible avec u...
herbelin
2002-06-13
*
Ajout map_inductive_type et map_ind_family
herbelin
2002-06-13
*
L'ordre supérieur avait quelque peu été oublié dans l'unification...
herbelin
2002-06-07
*
Mise au point de declare_red_expr
herbelin
2002-05-30
*
Finalement un seul constr pour l'instant dans ExtraRedExpr
herbelin
2002-05-30
*
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
*
Simplification du filtrage si la premiere ligne de motifs est inevitable + au...
herbelin
2002-05-03
*
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
[prev]
[next]