index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
LetIn dans Simpl
mohring
2000-12-14
*
Bug Inversion en présence de méta-variables
herbelin
2000-12-13
*
conflit useInversionLemma
mohring
2000-12-13
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Hint Unfold Local + commentaires
mohring
2000-12-12
*
Reparation Intro sans nom qui ne reduisait pas le but quand celui-ci
mohring
2000-12-12
*
message d'erreur
herbelin
2000-12-06
*
Divers bugs LetTac
herbelin
2000-12-06
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
Portage d'AutoRewrite
delahaye
2000-12-02
*
Nouveau long long avec Coq en tête
herbelin
2000-11-29
*
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-28
*
Elimination du '
delahaye
2000-11-28
*
Prise en compte des let-in dans les fonctions de réduction pour les tactiques
herbelin
2000-11-27
*
Appel des constantes globaux par des noms absolus
herbelin
2000-11-26
*
Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...
herbelin
2000-11-26
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
Nouveau choix pour l'intros initial
delahaye
2000-11-24
*
On n'introduit que des produits non dependants
delahaye
2000-11-23
*
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-23
*
Reparation IsMutConstruct + Transparent
mohring
2000-11-23
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
PatternMatchingFailure n'etait pas rattrapee
herbelin
2000-11-21
*
Bugs make_tuple et existS_pattern
herbelin
2000-11-21
*
Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...
herbelin
2000-11-20
*
Utilisation de global_reference dans pattern
herbelin
2000-11-20
*
Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...
herbelin
2000-11-20
*
methode export
filliatr
2000-11-15
*
Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...
herbelin
2000-11-10
*
Bug et simplification nouvel Induction
herbelin
2000-11-09
*
Nettoyage Names suite
herbelin
2000-11-07
*
Changement/extension dans les noms de parseurs de Grammar
herbelin
2000-11-07
*
Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....
herbelin
2000-11-06
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
compilation des fichiers ml4 sans GNUseries
filliatr
2000-11-03
*
correction Abstract (et make world passe!)
filliatr
2000-11-02
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
- simplification Makefile (compilation des fichiers .ml'; pas encore parfait
filliatr
2000-10-31
*
.old virés (CVS est là pour ca)
filliatr
2000-10-31
*
Remplacement de Tauto et Intuition
delahaye
2000-10-30
*
erreur dans intro_gen corrigée
filliatr
2000-10-27
*
Intro choue si le nom d'hypothse existe au lieu de mettre un avertissement
herbelin
2000-10-27
*
Ajoute : Ast dans la regle de grammaire
mayero
2000-10-27
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Changement parser par défaut dans Syntax
herbelin
2000-10-18
*
Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...
herbelin
2000-10-13
*
C'était pas le bon env dans build_term
herbelin
2000-10-11
*
Prise en compte de Let à certains endroits
herbelin
2000-10-11
*
Prise en compte de l'env local dans make_apply_entry
herbelin
2000-10-11
[next]