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
...
*
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
*
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
[prev]
[next]