index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
...
*
bug head_pattern_bound
herbelin
2000-12-25
*
Token n'est plus un keyword
herbelin
2000-12-25
*
Effet réorganisation Classops
herbelin
2000-12-25
*
*** empty log message ***
mayero
2000-12-22
*
Qualification des inductifs dans Print ind
herbelin
2000-12-21
*
espacements
herbelin
2000-12-20
*
Suppression warning variable de filtrage en majuscule
herbelin
2000-12-20
*
ajout ident_or_constrarg pour NewInduction
herbelin
2000-12-20
*
Amélioration affichage Print ALl
herbelin
2000-12-19
*
Correction associativite de Repeat/Orelse
delahaye
2000-12-19
*
Suppression de l'affichage des instances des ?n
herbelin
2000-12-18
*
Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite
herbelin
2000-12-16
*
Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...
herbelin
2000-12-15
*
Les params d'inductif deviennent en même temps propre à chaque inductif d'u...
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
*
Autorisation de parenthèses autour des constructeurs dans le filtrage
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
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
numarg -> pure_numarg a poursuivre
mohring
2000-12-11
*
Modif rapide pour prise en compte eqT
herbelin
2000-12-06
*
MAJ nom long de eq
herbelin
2000-12-06
*
section_path etait en fait bonne dans ast et buggee dans printer.ml
herbelin
2000-12-06
*
2ème bug de traduction des Path
herbelin
2000-12-06
*
Bug de traduction des Path
herbelin
2000-12-06
*
Extension de la syntaxe de LetTac
herbelin
2000-12-06
*
Notion de 'clause_pattern' pour désigner un ensemble d'occurrences dans le b...
herbelin
2000-12-06
*
Correction pour les qualidconstarg
delahaye
2000-12-06
*
Plus de quote devant les ident et les ?
delahaye
2000-12-05
*
Prise en compte REQUIRE dans print_leaf
herbelin
2000-11-29
*
ajout
filliatr
2000-11-29
*
Now AddRecPath and AddPath can be used with an As option to specify the
sacerdot
2000-11-29
*
Prise en compte du repertoire dans le section path; utilisation de dirpath po...
herbelin
2000-11-28
*
Ajout des Fix et CoFix dans les patterns
delahaye
2000-11-28
*
Elimination du '
delahaye
2000-11-28
*
Bug affichage inductifs
herbelin
2000-11-27
*
uniformisation messages d'erreur
filliatr
2000-11-27
*
Prise en compte des implicites de locaux à l'affichage
herbelin
2000-11-27
*
Affichage des définitions locales
herbelin
2000-11-27
*
Restruration autour de qualidarg
herbelin
2000-11-26
*
Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...
herbelin
2000-11-26
*
Prise en compte noms longs dans divers fonctions de Print
herbelin
2000-11-26
*
Réorganisation autour de globalize_constr
herbelin
2000-11-24
*
Nettoyage
herbelin
2000-11-24
*
Ajout d'un .:/opt/kde/bin:/home/herbelin/bin:/bin:/sbin:/usr/bin:/usr/etc:/us...
herbelin
2000-11-24
*
Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametab
filliatr
2000-11-24
*
certains effets disparaissent a la sortie des sections, d'autres non (selon S...
filliatr
2000-11-24
*
SearchPattern et SearchRewrite
filliatr
2000-11-24
*
Ajout d'une syntaxe pour Reals.
mayero
2000-11-23
[prev]
[next]