index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
MAJ crédits, fresh; documentation apply in
herbelin
2006-10-26
*
MAJ
herbelin
2006-10-26
*
Petit bug apply in
herbelin
2006-10-26
*
Applatissement des noeuds application vide dans le filtrage Ltac (ex:
herbelin
2006-10-25
*
Suite commit 9277
herbelin
2006-10-25
*
oups, ne chargeait pas les bons fichiers
letouzey
2006-10-25
*
Correction d'une tentative incorrecte (révision 9266) de clarification
herbelin
2006-10-25
*
coqdep -slash
barras
2006-10-25
*
Ménage
notin
2006-10-25
*
oops
barras
2006-10-25
*
conflit de nom (Field_theory) modulo la casse
barras
2006-10-25
*
Extension de fresh (suite)
herbelin
2006-10-24
*
Changement de la valeur par défaut de with_geoproof (stabilité coqide)
notin
2006-10-24
*
Test apply in
herbelin
2006-10-24
*
Insère une coercion vers Sortclass dans 'contradiction' si nécessaire
herbelin
2006-10-24
*
Ajout de la tactique 'remember'
herbelin
2006-10-24
*
Extension de la primitive ltac fresh pour qu'elle accepte une liste de
herbelin
2006-10-24
*
Ajout de la tactique "apply in".
herbelin
2006-10-24
*
Hack peu élégant pour permettre de parser des listes avec séparateurs dans
herbelin
2006-10-24
*
Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén...
herbelin
2006-10-24
*
fixed same_file (#1141)
barras
2006-10-23
*
fixed non-bug #1213
barras
2006-10-23
*
bug #1194: normalisation evars a la sortie de focus
barras
2006-10-23
*
Fixed "Show intros" which did not look at hypothesis.
courtieu
2006-10-23
*
Add a flush after backtracking x y z and before printing subgoals.
courtieu
2006-10-23
*
Add a flush for a warning.
courtieu
2006-10-23
*
Le calcul de la classe dans class_args_of ne suivait pas celui de class_of
herbelin
2006-10-21
*
Pas d'@ dans les identificateurs (pour F4 and co)
herbelin
2006-10-21
*
Correction d'un vieux bug de coercion avec éta-expansion (utilisation
herbelin
2006-10-21
*
MAJ
herbelin
2006-10-20
*
Correction du bug #1255 (réécriture setoid sous un produit)
notin
2006-10-20
*
Correction de la localisation des erreurs en interactif (numéro de
herbelin
2006-10-20
*
Starting to add a function schemes merging command (not finished, not
courtieu
2006-10-20
*
Correction sym -> comm
herbelin
2006-10-19
*
coqide: affichage des sous-buts et hypothèses et métas comme types de
herbelin
2006-10-19
*
field_simplify_eq profite de la factorisation de Laurent
barras
2006-10-17
*
Clarification des contraintes sur le contexte de paramètres des
herbelin
2006-10-17
*
Noms "canoniques" pour certaines des propriétés de xor.
herbelin
2006-10-17
*
Mise en forme des theories
notin
2006-10-17
*
affichage des ... dans les scripts
barras
2006-10-16
*
typo doc + bug legacy field
barras
2006-10-16
*
changes the use of lists and notations, to avoid that the notations
bertot
2006-10-16
*
Simplification ocamldebug (coq-debug-programs.out obsolète)
herbelin
2006-10-13
*
Ajout des options Coqide suggérées par Damien Doligez (wish #1053)
notin
2006-10-13
*
Adaptation des tests suite à la modification de Rewrite .. in (r9201)
notin
2006-10-13
*
Correction test-suite suite à r9186
notin
2006-10-13
*
Ajout du théorème mult_minus_distr_l
notin
2006-10-13
*
r9778@tannat: jforest | 2006-10-13 11:36:37 +0200
jforest
2006-10-13
*
Protection raise en début de séquence (en attendant que le code caché trou...
herbelin
2006-10-12
*
Fix name clash on left
thery
2006-10-12
[next]