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
*
Bug predicat let-tuple
herbelin
2003-09-09
*
Ajout construction If primitive dans constr_expr et rawconstr
herbelin
2003-09-09
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Mise en place possibilité de définitions locales dans les paramètres des i...
herbelin
2003-09-06
*
V8: FUNCLASS -> Funclass, SORTCLASS -> Sortclass
herbelin
2003-08-31
*
Bug et améliorations diverses
herbelin
2003-08-12
*
Bug détypage du fix
herbelin
2003-08-12
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Pb quand une meme classe est definie dans 2 fichiers
herbelin
2003-06-11
*
Simplification case_info
herbelin
2003-06-10
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Factorisation de detype_case pour utilisation par l'afficheur de pattern
herbelin
2003-06-10
*
Amélioration afficheur de Cases pour les constr_pattern
herbelin
2003-06-10
*
Tables logarithmiques pour les coercions + nettoyage
herbelin
2003-06-08
*
Preservation affichage des ?n en V7
herbelin
2003-05-22
*
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
*
Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...
herbelin
2003-04-27
*
simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...
letouzey
2003-04-16
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Correction bug #261 + amélioration nommage
herbelin
2003-04-01
*
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin
2003-03-29
*
*** empty log message ***
barras
2003-03-21
*
*** empty log message ***
barras
2003-03-12
*
Bug affichage let destructurant
herbelin
2003-02-02
*
Backtrack sur le filtrage des applications partielles (change Tauto/Intuition)
herbelin
2003-02-01
*
Ajout d'un filtrage d'application partielle
herbelin
2003-01-31
*
Unification plus efficace vis à vis du LetIn
herbelin
2003-01-31
*
reparation des contribs: lors de l'unification, reduire les beta redexes
barras
2003-01-23
*
modified the unification algorithm to try first order unification before
barras
2003-01-22
*
ajout de whd_state dans l'interface
barras
2003-01-22
*
Localisation
herbelin
2003-01-19
*
Problème de désynchronisation des variables du type et du corps d'un point-...
herbelin
2003-01-15
*
Bug en présence de let-in
herbelin
2003-01-15
*
Prise en compte application partielle dans dependent
herbelin
2002-12-23
*
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
[next]