index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2000-10-18
Nettoyage
herbelin
2000-10-18
globalize_command devient globalize_constr
herbelin
2000-10-18
Correction pb de globalisation dans print_mutual
herbelin
2000-10-18
MAJ
herbelin
2000-10-17
Pb factorisation de Print Grammar
herbelin
2000-10-16
MAJ
herbelin
2000-10-16
Changement "command" en "constr" et globalize_command en globalize_constr
herbelin
2000-10-16
Correction bug affichage des infix
herbelin
2000-10-13
Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...
herbelin
2000-10-13
Code redondant
herbelin
2000-10-13
Suppression d'un test inutile dans RCast
herbelin
2000-10-13
Code redondant
herbelin
2000-10-13
Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...
herbelin
2000-10-13
TODO
herbelin
2000-10-12
Parentheses
herbelin
2000-10-12
Hypotheses des ind oubliees dans le discharge
herbelin
2000-10-11
Idem pour défs locales dans Var
herbelin
2000-10-11
MAJ
herbelin
2000-10-11
Nouveau type rec_declaration
herbelin
2000-10-11
Renommage des find_m*type
herbelin
2000-10-11
Suite du précédent
herbelin
2000-10-11
Delta des défs locales en de Bruijn toujours pas stable
herbelin
2000-10-11
Ajout push_rec_types
herbelin
2000-10-11
Ajout mind_arities_env
herbelin
2000-10-11
Renommage des find_m*type
herbelin
2000-10-11
Prise en compte de l'environnement dans le calcul des implicites
herbelin
2000-10-11
Prise en compte de l'environnement dans les tests de bonne fondaison
herbelin
2000-10-11
Prise en compte de l'environnement dans les tests de correction des inductifs
herbelin
2000-10-11
C'était pas le bon env dans build_term
herbelin
2000-10-11
Niveau d'associativité du let
herbelin
2000-10-11
Prise en compte de Let à certains endroits
herbelin
2000-10-11
Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)
herbelin
2000-10-11
Prise en compte de l'env local dans make_apply_entry
herbelin
2000-10-11
Message d'erreur bad pattern
herbelin
2000-10-11
Prise en compte de Let dans build_dependent_inductive
herbelin
2000-10-11
Bug affichage du nom des letin
herbelin
2000-10-11
Bug dans [prvecti v] quand v est vide
herbelin
2000-10-10
MAJ
herbelin
2000-10-10
Correction de bugs (alias initiaux et ordre des cas par défaut)
herbelin
2000-10-10
Plus d'échec sur les globaux lorsque prterm est appelé par le débugger
herbelin
2000-10-10
Bug ordre dans push_rels
herbelin
2000-10-10
Finalement, encore un Simpl inutile
herbelin
2000-10-10
Messages d'erreurs Cases
herbelin
2000-10-06
MAJ
herbelin
2000-10-06
Correction incompatibilites dans la fn des types des inductifs
herbelin
2000-10-06
MAJ pour nouvelle syntaxe des membres droits des grammaires
herbelin
2000-10-06
Parenthèses pour les tactiques
herbelin
2000-10-06
Mise en page de Print Hint
herbelin
2000-10-06
Changement dans la stratégie de réduction du Fix par Simpl
herbelin
2000-10-06
Bug splay_prod_assum
herbelin
[next]