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
*
Le test de redondance d'une règle était trop fort
herbelin
2002-10-23
*
Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...
herbelin
2002-10-22
*
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
herbelin
2002-10-21
*
NewDestruct/NewInduction acceptent l'option "using"
herbelin
2002-10-21
*
Prise en compte des délimiteurs dans les motifs de Cases
herbelin
2002-10-21
*
Prise en compte des délimiteurs dans les motifs de Cases
herbelin
2002-10-21
*
L'application de ltac attend une référence; meilleure protection contre
herbelin
2002-10-14
*
Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une
herbelin
2002-10-14
*
Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage
herbelin
2002-10-13
*
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...
herbelin
2002-10-13
*
réparation de la protection contre les clauses indiscernables de TACTIC EXTE...
herbelin
2002-10-12
*
Notation 2:Check et 2:Eval
herbelin
2002-10-12
*
Restriction sur la forme des Syntactic Definition et re-localisation en fonct...
herbelin
2002-10-12
*
Lazy manuelles dans le code
coq
2002-10-07
*
Lazy experimentale temporaire...
coq
2002-10-05
*
pretty s'appellait prettyp mais il est revenu sous son ancien nom
herbelin
2002-10-05
*
passage a ocaml 3.06
herbelin
2002-09-27
*
Un peu (plus) d'ordre dans Nametab...
coq
2002-09-24
*
La notation with dependante + affichage dependante de moduels corrige
coq
2002-09-20
*
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-19
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Réparation d'un bug qui considérait les composantes d'un QUALID
herbelin
2002-07-30
*
Pb de factorisation camlp4
herbelin
2002-07-15
*
Pour assurer une compatibilite avec la 7.3
herbelin
2002-07-15
*
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
herbelin
2002-07-11
*
Coercion de la syntaxe des motifs non atomiques
herbelin
2002-06-19
*
Petits beug d'affichages.
gregoire
2002-06-13
*
Correction mauvais ordre dans le parsing des dirpath; MAJ de la quotification
herbelin
2002-06-05
*
Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct
herbelin
2002-06-05
*
Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...
herbelin
2002-06-05
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Finalement un seul constr pour l'instant dans ExtraRedExpr
herbelin
2002-05-30
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Implante la macro camlp4 VERNAC COMMAND EXTEND
herbelin
2002-05-29
*
Implante la macro camlp4 TACTIC EXTEND
herbelin
2002-05-29
*
Ajout de Eval, Inst et Check
delahaye
2002-05-27
*
Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
herbelin
2002-05-15
*
Utilisation d'une construction spéciale SECVAR pour gérer la
herbelin
2002-05-14
*
Plus de souplesse pour les constructeurs encapsulés sous des définitions
herbelin
2002-05-10
*
Suppression d'un warning plus surprenant qu'utile
herbelin
2002-04-18
*
Typo
herbelin
2002-04-16
*
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2002-04-10
*
Syntactic Definition autorisée dans les motifs de Cases (utile notamment
herbelin
2002-04-10
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
Correction bug infix sur des varaiables
mohring
2002-03-29
*
Ajout de l'entrée ne_constrarg_list
delahaye
2002-03-19
*
Meilleure gestion de la reduction dans Field
delahaye
2002-03-17
[next]