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
*
Substitution dans REvar et PEvar plutot que encodage via noeud application po...
herbelin
2003-12-19
*
name_app accessible a tous dans Nameops
herbelin
2003-12-19
*
ajout test de non-regression Clear d'une def locale
barras
2003-12-17
*
MAJ suppression 250
herbelin
2003-12-16
*
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
barras
2003-12-15
*
correction bug: parentheses ne cassent plus les implicites
barras
2003-12-08
*
Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...
herbelin
2003-12-04
*
Symetrisation parsing/printing 'abstract'
herbelin
2003-12-04
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
Ajout ne_string
herbelin
2003-11-27
*
Protection contre les notations vides
herbelin
2003-11-26
*
Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...
herbelin
2003-11-26
*
modif lexer: ident peut commencer par _
barras
2003-11-25
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
Prise en compte des definitions locales dans les (co-)points-fixes
herbelin
2003-11-23
*
Suppression des niveaux vides
herbelin
2003-11-21
*
Ajout Print Implicit
herbelin
2003-11-21
*
Pas d'entrees autres que les predefinies en v8
herbelin
2003-11-21
*
Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...
herbelin
2003-11-20
*
Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...
herbelin
2003-11-19
*
Protection contre l'effacement des niveaux vides de operconstr et pattern par...
herbelin
2003-11-19
*
reparation bug moins unaire (erreur de PP)
barras
2003-11-18
*
Code mort
herbelin
2003-11-18
*
New tactics : econstructor, eleft, eright, esplit
clrenard
2003-11-17
*
Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)
herbelin
2003-11-17
*
Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar
herbelin
2003-11-15
*
Ajout Print Implicit avec depliage du type
herbelin
2003-11-15
*
Compatibilite %T
herbelin
2003-11-14
*
Bug parsing cast
herbelin
2003-11-14
*
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...
barras
2003-11-13
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Suppression du "..." final !
herbelin
2003-11-12
*
Mise en place systeme de renommage des noms de variables liees dans la biblio...
herbelin
2003-11-12
*
MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter l...
herbelin
2003-11-12
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
petits changements de syntaxe
barras
2003-11-12
*
Suppression SearchNamed finalement redondant avec SearchAbout
herbelin
2003-11-10
*
Traduction semantique des InHyp de clause en InHypValue si local def
herbelin
2003-11-09
*
'as' avant 'using' dans 'destruct'
herbelin
2003-11-09
*
Fusion de tuple_constr/tuple_pattern dans operconstr/pattern
herbelin
2003-11-08
*
Added Instantiate ... in
corbinea
2003-11-06
*
Interpretation des entiers dans N (ex-entier), maj du module des positive
herbelin
2003-11-05
*
En v8, une notation, c'est 2 regles et un niveau
herbelin
2003-11-04
*
Explicitation message d'erreur nombres negatifs
herbelin
2003-11-04
*
Compatibilite V7.4 pour le delimiteur de positive
herbelin
2003-11-03
*
Le printeur de Show Script n'etait pas le bon en v7
herbelin
2003-11-02
*
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
[next]