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
*
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
*
Mise a jour
mohring
2000-12-15
*
Printer
mohring
2000-12-15
*
test univers, inductifs et sections
filliatr
2000-12-15
*
MAJ
herbelin
2000-12-14
*
Bug sur commit précédent
herbelin
2000-12-14
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
Mauvais env donné à new_isevar
herbelin
2000-12-14
*
Oubli test de correction à l'instantiation des evars
herbelin
2000-12-14
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
herbelin
2000-12-14
*
Mise en page
herbelin
2000-12-14
*
Amélioration message d'erreur
herbelin
2000-12-14
*
Évaluation forcée des objets mis dans les streams
herbelin
2000-12-14
*
Amélioration message d'erreur
herbelin
2000-12-14
*
Mise a jour
mohring
2000-12-14
*
LetIn dans Simpl
mohring
2000-12-14
*
Bug sur commit précédent
herbelin
2000-12-14
*
Enfin trouvé la cause d'exception; suppression de la capsule de rattrapage
herbelin
2000-12-14
*
MAJ commentaires
herbelin
2000-12-14
*
MAJ
herbelin
2000-12-14
*
Fichier de test pour les Cases
herbelin
2000-12-14
*
Autorisation de parenthèses autour des constructeurs dans le filtrage
herbelin
2000-12-14
*
Raffinement erreur Wrong Predicate
herbelin
2000-12-14
*
Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...
herbelin
2000-12-14
*
Bug dans les alias de Cases
herbelin
2000-12-14
*
On force l'évaluation du qualid_of_global qui peut échouer dans le débugger
herbelin
2000-12-14
*
Bug Inversion en présence de méta-variables
herbelin
2000-12-13
*
conflit useInversionLemma
mohring
2000-12-13
*
mise a jour
filliatr
2000-12-12
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
*** empty log message ***
mohring
2000-12-12
[next]