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
*
Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8
herbelin
2003-11-01
*
Il ne faut pas mettre le constrarg des tactiques au niveau lconstr
herbelin
2003-11-01
*
Extensibilite de la grammaires des patterns
herbelin
2003-11-01
*
Traduction des noms pour les refs de pr_glob_generic (via pr_global)
herbelin
2003-11-01
*
Utilisation de niveaux pour l'extensibilite de la grammaires des patterns
herbelin
2003-11-01
*
Extension de get_constr_entry et symbol_of_production pour gerer les extensio...
herbelin
2003-11-01
*
Heritage des notations v7 seulement si zero information v8
herbelin
2003-11-01
*
Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...
herbelin
2003-10-30
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Saut de ligne avant les infos non logiques de print_about
herbelin
2003-10-23
*
Conjecture declare maintenant un axiome; reorganisation VernacDefinition
herbelin
2003-10-23
*
Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition
herbelin
2003-10-23
*
Independance de grammar.cmo vis a vis de Search
herbelin
2003-10-23
*
Suppression dependance formelle en Vernacexpr
herbelin
2003-10-22
*
Integration de SearchNamed dans SearchAbout
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...
herbelin
2003-10-21
*
Extension de Locate
herbelin
2003-10-21
*
On n'autorise plus les niveaux doubles L/R en v8
herbelin
2003-10-17
*
Bug mot-cle TYPES
herbelin
2003-10-17
*
Traduction des idents aussi dans le printer generique des tactiques
herbelin
2003-10-17
*
nouvelle syntaxe de ltac
barras
2003-10-16
*
lettac -> set
barras
2003-10-16
*
Bug Search
herbelin
2003-10-16
*
Mise en conformite return_type en fonction de la doc
herbelin
2003-10-15
*
Changement 'as notation' en 'where notation'
herbelin
2003-10-14
*
Ameliration affichage inductifs
herbelin
2003-10-13
*
Ajout d'une fonction de recherche sur les composantes du nom des objets
herbelin
2003-10-13
*
Ajout d'une fonction de recherche sur les composantes du nom des objets
herbelin
2003-10-13
*
Ajout fnl() dans About
herbelin
2003-10-11
*
mise a jour nouvelle syntaxe
barras
2003-10-11
*
Suppression Grammar/Syntax
herbelin
2003-10-10
*
Delimiters N devient 'nat'
herbelin
2003-10-10
*
Cablage en dur de inversion
herbelin
2003-10-10
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Compatibilite ocaml 3.06 et 3.07
herbelin
2003-10-09
*
Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...
herbelin
2003-10-08
*
Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'
herbelin
2003-10-07
*
Debranchement de l'affichage automatique de Proof par le traducteur (trop com...
herbelin
2003-10-07
*
Inspect saute maintenant les marqueurs invisibles
herbelin
2003-10-07
*
Hypothesis mot-cle
herbelin
2003-10-02
*
Implantation de l'option 'format' des Notations
herbelin
2003-10-01
*
Les notations hors scope s'empilent maintenant comme des scopes ne
herbelin
2003-09-30
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Bug about
herbelin
2003-09-26
*
Syntaxe plus liberale pour le type des arguments de filtrage du 'match'
herbelin
2003-09-26
*
Ajout 'About'
herbelin
2003-09-26
*
Re-possibilite changement chaine infixe en passant v7 a v8
herbelin
2003-09-26
*
Utilisation de noms dans 'Implicit Arguments [...]'
herbelin
2003-09-24
*
Utilisation de noms dans 'Implicit Arguments [...]'
herbelin
2003-09-23
[next]