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
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
bug coqmktop avec libcoqrun.a en bytecode
barras
2004-11-15
*
Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...
herbelin
2004-11-15
*
*** empty log message ***
gregoire
2004-11-12
*
Changement dans les boxed values .
gregoire
2004-11-12
*
Correction bug #868
herbelin
2004-11-10
*
MAJ
herbelin
2004-11-09
*
code mort
herbelin
2004-11-09
*
Prise en compte des notations récursives dans l'option 'format'
herbelin
2004-11-08
*
MAJ commentaire sur incohérence EM dans Set
herbelin
2004-11-07
*
autorewrite moved from HIGHTACTICS to TACTICS (to implement Printing
sacerdot
2004-11-05
*
Univ.pr_univ ==> Univ.pr_uni
sacerdot
2004-11-04
*
Affichage des univers
herbelin
2004-11-04
*
Réponse à la conjecture que PI est indépendant de EM dans CC
herbelin
2004-11-02
*
qq bugs du highlight de CoqIDE
filliatr
2004-10-28
*
Added code to get rid of duplicate rewriting rules.
sacerdot
2004-10-28
*
Ajout 'dependent rewrite in'
herbelin
2004-10-28
*
maj
filliatr
2004-10-27
*
Factorisation cut_replacing
herbelin
2004-10-27
*
Restructuration fonctions de réécriture depuis égalité dépendante
herbelin
2004-10-27
*
Restructuration fonctions de réécriture depuis égalité dépendante; facto...
herbelin
2004-10-27
*
Ajout test dependent rewrite
herbelin
2004-10-27
*
Bug mauvais nom d'entrée binder_constr quand récursion gauche
herbelin
2004-10-27
*
Non affichage des notations réduites à une variable
herbelin
2004-10-27
*
maj
filliatr
2004-10-26
*
maj
filliatr
2004-10-25
*
Word "setoid" banned from the error messages. "relation" used instead.
sacerdot
2004-10-25
*
Added option -no-vm.
sacerdot
2004-10-25
*
Missing check implemented (closes a bug from Bas Spitters).
sacerdot
2004-10-25
*
maj
filliatr
2004-10-24
*
maj
filliatr
2004-10-22
*
maj
filliatr
2004-10-21
*
The morphism lemma type was simplified only in modules and not in module
sacerdot
2004-10-21
*
Error message improved.
sacerdot
2004-10-21
*
maj
filliatr
2004-10-20
*
maj
filliatr
2004-10-20
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)
barras
2004-10-20
*
The bug already closed in revision 1.90 was reintroduced again.
sacerdot
2004-10-20
*
maj
filliatr
2004-10-19
*
Proof term size reduction (again).
sacerdot
2004-10-19
*
maj
filliatr
2004-10-18
*
maj
filliatr
2004-10-18
*
* Code simplification and clean-up. In particular there is no more code
sacerdot
2004-10-18
*
Code simplification and clean-up.
sacerdot
2004-10-18
*
The lem field was not computed properly for morphisms whose argument was
sacerdot
2004-10-18
*
The "lem" field of a morphism used to be the compatibility proof, but it
sacerdot
2004-10-18
*
Bug fixed: relations quantified more than once where abstracted in the wrong
sacerdot
2004-10-18
*
More informative error message when the tactic tries to generate a new
sacerdot
2004-10-18
*
zeta flag added to reduce LetIns in a morphism type. Morphisms with local
sacerdot
2004-10-18
[next]