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
*
supression vieux fichiers extraction
filliatr
2001-04-04
*
rollback sur les commandes Extract Constant/Inductive; nettoyage et documenta...
filliatr
2001-04-04
*
deux fichiers (past et ptype) uniquement sous forme de .mli
filliatr
2001-04-04
*
commandes Extract Constant/Inductive; message d'erreur pour les axiomes
filliatr
2001-04-03
*
The function filter_by_module, that was previously exported was not the
bertot
2001-04-03
*
Export a function (build_inductive) that is used in the graphical interface.
bertot
2001-04-03
*
Make sure that the COQTOP variable is really used, when it is set.
bertot
2001-04-03
*
Make it possible to perform proofs by induction even on non-inductive types,
bertot
2001-04-03
*
ménage
filliatr
2001-04-03
*
psyntax.ml4 sous CVS
filliatr
2001-04-03
*
utilisation de Options.if_verbose
filliatr
2001-04-03
*
installation des .cmo pour l'extraction
filliatr
2001-04-03
*
mise a jour pour ocamlweb
filliatr
2001-04-02
*
mise a jour
filliatr
2001-04-02
*
parenthèses autour des types dans les arguments des constructeurs
filliatr
2001-04-02
*
underscores pour les variables représentant des propositions
filliatr
2001-04-02
*
inductifs vides
filliatr
2001-04-02
*
ml_pop au lieu de ml_lift dans betared_ast
filliatr
2001-04-02
*
à faire
filliatr
2001-04-02
*
bug Fix signalé par Alexandre (even/odd mal interprété)
filliatr
2001-04-02
*
branchement extraction (bytecode seulement)
filliatr
2001-03-30
*
Ajout de lemmes sur les booleens
mohring
2001-03-30
*
Introduction d'une preuve de False_rec
mohring
2001-03-30
*
extraction modulaire
filliatr
2001-03-30
*
extraction modulaire + environnement des Fix corrigé
filliatr
2001-03-30
*
repertoire pour les tests d'extraction
filliatr
2001-03-30
*
application avec bcp args
letouzey
2001-03-30
*
beta-reduction
filliatr
2001-03-30
*
mise en place de Correctness (ne compile pas encore)
filliatr
2001-03-29
*
deux fois $Id$
filliatr
2001-03-29
*
fichiers extraction
filliatr
2001-03-29
*
changement type_var et signature
filliatr
2001-03-28
*
amelioration de la structure des univers
barras
2001-03-28
*
Interprétation des qualidarg
herbelin
2001-03-27
*
conservation des arguments dans Prop (snif)
filliatr
2001-03-27
*
mise a jour
filliatr
2001-03-27
*
extraction recursive d'un morceau d'environnement
filliatr
2001-03-27
*
trace des inductifs sur Prop
letouzey
2001-03-27
*
Bibliotheque Num
mohring
2001-03-26
*
cache pour les constantes
filliatr
2001-03-26
*
ocaml 3.01 requis
herbelin
2001-03-25
*
Tag pour une beta3-ocaml3.01
herbelin
2001-03-25
*
MAJ
herbelin
2001-03-23
*
MAJ
herbelin
2001-03-23
*
Les règles d'affichage ajoutés dans le commit précédent avait le même no...
herbelin
2001-03-23
*
amelioration de la consommation memoire de la conversion en eta-expansant
barras
2001-03-23
*
mise a jour
filliatr
2001-03-23
*
eta-expansion des constructeurs si necessaire (a posteriori en miniML)
filliatr
2001-03-23
*
La strategie de recherche de lookup_eliminator etait insuffisante
herbelin
2001-03-23
*
suppression des param dans inductifs. suite du Cases
letouzey
2001-03-23
[next]