index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
Backtrack sur le passage de Set à Type pour l'ordre lexicographique
herbelin
2007-02-07
*
Passage de Set à Type dans Relations et Wellfounded
herbelin
2007-02-06
*
Correction typo eq_rec_eq (cf bug #1339)
herbelin
2007-01-31
*
Derivation of (exists x : A, P x) -> {x : A | P x} for decidable P
emakarov
2007-01-23
*
Clarification redondance Axiome du choix unique/description
herbelin
2007-01-22
*
Add f_equal case for 6 arguments.
msozeau
2007-01-02
*
Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à
herbelin
2006-12-28
*
Remplacement de la définition de Pind et Prec par une définition
herbelin
2006-12-28
*
Changement dans ring et field, beaucoup de correction d'erreurs,
bgregoir
2006-12-15
*
Dépendence inutile
herbelin
2006-12-12
*
AllÃègement de syntxe suite à l'introduction de l'unif pattern
herbelin
2006-12-12
*
Bug nommage Zgt_trans_succ
herbelin
2006-12-12
*
correction Open Local Scope (Ring)
bgregoir
2006-12-11
*
Changement dans le kernel :
bgregoir
2006-12-11
*
fixes PR#1269 about function: there is no reason well founded induction is
bertot
2006-11-05
*
fixed field_simplify + changed precedence of let and fun in ltac
barras
2006-10-30
*
LegacyRfield was opening R_scope
barras
2006-10-30
*
simplif de la partie ML de ring/field
barras
2006-10-27
*
Le caractère ² fait planter make doc
notin
2006-10-27
*
Déplacement des propriétés générales de BinList dans List et des tactiqu...
herbelin
2006-10-26
*
oups, ne chargeait pas les bons fichiers
letouzey
2006-10-25
*
Ajout de la tactique 'remember'
herbelin
2006-10-24
*
Noms "canoniques" pour certaines des propriétés de xor.
herbelin
2006-10-17
*
Mise en forme des theories
notin
2006-10-17
*
Ajout du théorème mult_minus_distr_l
notin
2006-10-13
*
revert, the previous commit was a mistake
bertot
2006-10-05
*
A version of natprering that should be more efficient and removal of a bad
bertot
2006-10-05
*
revision de la semantique de rewrite ... in <clause>. details dans la doc
letouzey
2006-10-05
*
Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom
barras
2006-10-05
*
args implicites dans Field
barras
2006-09-29
*
separation de RealField
barras
2006-09-28
*
commit de field + renommages
barras
2006-09-26
*
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-09-26
*
Ajout d'une valeur VList dans tacinterp pour permettre de cabler des
herbelin
2006-09-22
*
incomplete and temporary fix for PR#1222: revert accepts up to 10 args
letouzey
2006-09-21
*
better scope/require managment (patch by Russel O'Connor)
letouzey
2006-09-21
*
Indentation + typo
notin
2006-09-01
*
Passage à une définition de inhabited plus dans les 'standard mathématique...
herbelin
2006-08-28
*
"Essai de remplacement de "ex P" par "exists x, P x" suite à
herbelin
2006-08-28
*
JMeq maintenant applicable sur Type
herbelin
2006-08-24
*
comparison functions should be Defined not Qed
letouzey
2006-08-14
*
Renommage sqtr_lem_1 (bug 1189)
notin
2006-07-17
*
Ajout de quelques Arguments Scope pour simuler la récursivité du scope Rfun...
herbelin
2006-07-11
*
Argument Scope de list déplacé dans List.v
herbelin
2006-07-09
*
Typo
herbelin
2006-07-06
*
Quelques Hint inutiles
herbelin
2006-07-06
*
MAJ du manuel de référence
notin
2006-07-04
*
Ajout de Zgcd_spec (compat.)
notin
2006-06-26
*
nouvel algorithme pour Zgcd (plus rapide) + un Qcompare
letouzey
2006-06-25
*
repetition d'hypotheses dans well_founded_induction_type_2
letouzey
2006-06-25
[next]