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
*
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
*
Search réparé
filliatr
2000-11-23
*
Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_sp
herbelin
2000-11-23
*
Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;
herbelin
2000-11-23
*
Bug qualidconstarg (intervient pour Transparent)
herbelin
2000-11-23
*
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...
herbelin
2000-11-22
*
deplacement poly_args; iterateurs sur les segments
filliatr
2000-11-22
*
Begin-End Silent deviennent Set?Unset Silent
mohring
2000-11-21
*
Prise en compte des implicites dans les regles de grammaires
herbelin
2000-11-21
[next]