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
*
Simplifications
herbelin
2001-02-08
*
Scratch par defaut si rien n'est specifier dans Add LoadPath
herbelin
2001-02-08
*
Suppression warning no .coqrc
herbelin
2001-02-08
*
simplification du make depend; fonctions de stat. util. memoire dans certains...
filliatr
2001-02-08
*
modifs mineures
filliatr
2001-02-08
*
exporting traverse_to and mutate: they are used in pcoq.
bertot
2001-02-08
*
export a function that can be used to retrieve the context corresponding
bertot
2001-02-08
*
Meilleure approche du conflit path/freeze/library_root en séquentialisant la...
herbelin
2001-02-07
*
code mort
herbelin
2001-02-07
*
Ajout du Match Context
delahaye
2001-02-07
*
Reparation du pretty-print pour les tactiques
delahaye
2001-02-07
*
Modif pour les patterns de sous-termes
delahaye
2001-02-07
*
Probleme synchronisation roots / inputstate
herbelin
2001-02-07
*
Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir
herbelin
2001-02-07
*
Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir
herbelin
2001-02-07
*
Message d'erreur absolute_reference
herbelin
2001-02-07
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Chgt signature de type_of_existential
herbelin
2001-02-07
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
mise en place extraction
filliatr
2001-02-06
*
mise a jour
filliatr
2001-02-06
*
Correction pour les Unfold/Fold dans Cbv
delahaye
2001-02-06
*
EqDecide
filliatr
2001-02-06
*
Ajout d'un exemple
delahaye
2001-02-06
*
MAJ
herbelin
2001-02-06
*
Ajout d'une commande pour afficher chaque coercion à la demande
herbelin
2001-02-06
*
Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...
herbelin
2001-02-06
*
Extension coerce_to_var
herbelin
2001-02-05
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
Meilleur traitement des noms explicites dans la Nametab; Différentation du t...
herbelin
2001-02-05
*
Restructuration de classops; évolution en une version mieux intégrée au re...
herbelin
2001-02-05
*
Correction pour Time pour ne pas etre oblige de mettre deux points
delahaye
2001-02-05
*
calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)
filliatr
2001-02-05
*
D'autres exemples
delahaye
2001-02-05
*
Pas d'Apply dans Tauto
delahaye
2001-02-05
*
Ajout d'une heuristique pour les types dependants
delahaye
2001-02-05
*
Ajout du test de Tauto
delahaye
2001-02-05
*
Message d'erreur plus explicite pour Tauto
delahaye
2001-02-05
*
rétablissement patch Claudio
filliatr
2001-02-05
*
rétablissement nouveau Tauto
filliatr
2001-02-05
*
Résolution d'un bug de simplification
delahaye
2001-02-03
*
*** empty log message ***
mohring
2001-02-02
*
*** empty log message ***
mohring
2001-02-02
*
Ajout des credits version V6.3
mohring
2001-02-02
*
Retire le warning stat
mohring
2001-02-02
*
retablissement (provisoire) de l'ancien Ring a cause d'une explosion en temps...
filliatr
2001-02-02
*
Nouvelle beta
herbelin
2001-02-02
*
bug Variable + Record
filliatr
2001-02-01
*
application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés
filliatr
2001-02-01
[next]