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
*
Toujours Induction
herbelin
2000-12-20
*
ajout ident_or_constrarg pour NewInduction
herbelin
2000-12-20
*
Induction/NewInduction
herbelin
2000-12-20
*
Bug dans l'utilisation de l'option debug
herbelin
2000-12-20
*
Import module force l'ouverture du module même s'il était déjà ouvert afi...
herbelin
2000-12-20
*
Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints q...
herbelin
2000-12-20
*
Ajout set_lc
herbelin
2000-12-20
*
Scripts de correction d'uri
herbelin
2000-12-20
*
MAJ
herbelin
2000-12-20
*
Non verbose par défaut
herbelin
2000-12-20
*
Correction pour les variables abstraites dans les Tactic Definitions
delahaye
2000-12-19
*
DEMOS passe et MUTUAL-EXCLUSION aussi modulo Realizer
delahaye
2000-12-19
*
correction de bugs sur commit précédent
herbelin
2000-12-19
*
Découpage des différentes fonctionnalités de build_mutual et definition_st...
herbelin
2000-12-19
*
Export fonction testant si un inductive est un record
herbelin
2000-12-19
*
Amélioration affichage Print ALl
herbelin
2000-12-19
*
Pédagogie
herbelin
2000-12-19
*
Correction associativite de Repeat/Orelse
delahaye
2000-12-19
*
AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disque
delahaye
2000-12-19
*
Bugs connus et non résolus
herbelin
2000-12-18
*
MAJ
herbelin
2000-12-18
*
Renommages autour de NewInduction
herbelin
2000-12-18
*
Code mort
herbelin
2000-12-18
*
Documentation
herbelin
2000-12-18
*
Suppression de l'affichage des instances des ?n
herbelin
2000-12-18
*
MAJ
herbelin
2000-12-18
*
Amélioration message d'erreur mauvais prédicat
herbelin
2000-12-18
*
Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_name
herbelin
2000-12-18
*
Debut de nettoyage de Simpl
mohring
2000-12-18
*
Mise a jour
mohring
2000-12-18
*
Mise a jour
mohring
2000-12-18
*
MAJ
herbelin
2000-12-16
*
Redondant or incompatible instantiations in clenv_assign now correctly trapped
herbelin
2000-12-16
*
*** empty log message ***
herbelin
2000-12-16
*
Suppression du warning several default clauses
herbelin
2000-12-16
*
Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite
herbelin
2000-12-16
*
Le bon choix, c'est finalement identifier = string
herbelin
2000-12-15
*
Mise en page
herbelin
2000-12-15
*
Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...
herbelin
2000-12-15
*
Bug env vis à vis du let in
herbelin
2000-12-15
*
pb niveau
mayero
2000-12-15
*
suppression warning et calcule type dans replace_by_meta dans tous les cas
filliatr
2000-12-15
*
mise a jour
filliatr
2000-12-15
*
- suppression mind_extract_params
filliatr
2000-12-15
*
MAJ
herbelin
2000-12-15
*
Réparation de bugs de LoadPath
herbelin
2000-12-15
*
Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...
herbelin
2000-12-15
*
Petite réorganisation
herbelin
2000-12-15
*
Bug des locaux au premier niveau des modules qui disparaissaient de l'environ...
herbelin
2000-12-15
*
Bugs calcul du prédicat des Cases et Case
herbelin
2000-12-15
[next]